Merge pull request #591 from SkySkimmer/erelevance

Adapt to coq/coq#18938 (EConstr.ERelevance)

src/context_map.mli

@@ -99,9 +99,9 @@ val make_permutation : ?env:Environ.env -> Evd.evar_map ->
   context_map -> context_map -> context_map
 
 val specialize_mapping_constr : Evd.evar_map -> context_map -> constr -> constr
-val rels_of_ctx : ?with_lets:bool -> ('a,'b) Context.Rel.pt -> constr list
+val rels_of_ctx : ?with_lets:bool -> ('a,'b,'c) Context.Rel.pt -> constr list
 
-val patvars_of_ctx : ?with_lets:bool -> ('a,'b) Context.Rel.pt -> pat list
+val patvars_of_ctx : ?with_lets:bool -> ('a,'b,'c) Context.Rel.pt -> pat list
 (** Includes lets by default *)
 
 val pat_vars_list : int -> pat list
@@ -152,8 +152,8 @@ val new_strengthen :
   rel_context -> int -> ?rels:Int.Set.t -> constr ->
   context_map * context_map
 
-val id_pats : ('a, 'b) Context.Rel.pt -> pat list
-val id_subst : ('a, 'b) Context.Rel.pt -> ('a, 'b) Context.Rel.pt * pat list * ('a,'b) Context.Rel.pt
+val id_pats : ('a, 'b,'c) Context.Rel.pt -> pat list
+val id_subst : ('a, 'b, 'c) Context.Rel.pt -> ('a, 'b, 'c) Context.Rel.pt * pat list * ('a,'b,'c) Context.Rel.pt
 val eq_context_nolet :
   env ->
   Evd.evar_map -> rel_context -> rel_context -> bool

src/covering.ml

@@ -255,16 +255,16 @@ let lets_of_ctx env ctx evars s =
         | PRel i -> (ctx', cs, (i, id) :: varsubst, k, Id.Set.add id ids)
         | _ -> 
           let ty = e_type_of envctx evars c in
-          (make_def (Context.nameR id) (Some (lift k c)) (lift k ty) :: ctx', (c :: cs),
+          (make_def (nameR id) (Some (lift k c)) (lift k ty) :: ctx', (c :: cs),
            varsubst, succ k, Id.Set.add id ids))
       ([],[],[],0,Id.Set.empty) s
   in
   let _, _, ctx' = List.fold_right (fun decl (ids, i, ctx') ->
       let (n, b, t) = to_tuple decl in
-      try ids, pred i, (make_def (Context.nameR (List.assoc i varsubst)) b t :: ctx')
+      try ids, pred i, (make_def (nameR (List.assoc i varsubst)) b t :: ctx')
       with Not_found -> 
         let id' = Namegen.next_name_away n.Context.binder_name ids in
-        Id.Set.add id' ids, pred i, (make_def (Context.nameR id') b t :: ctx')) ctx (ids, List.length ctx, [])
+        Id.Set.add id' ids, pred i, (make_def (nameR id') b t :: ctx')) ctx (ids, List.length ctx, [])
   in pats, ctxs, ctx'
 
 let env_of_rhs evars ctx env s lets = 

src/covering.mli

@@ -35,7 +35,7 @@ val unify_constrs :
   rel_context ->
   constr list ->
   constr list -> context_map
-val flexible : pat list -> ('a,'b) Context.Rel.pt -> Int.Set.t
+val flexible : pat list -> ('a,'b,'c) Context.Rel.pt -> Int.Set.t
 val accessible : pat -> Int.Set.t
 val accessibles : pat list -> Int.Set.t
 val hidden : pat -> bool
@@ -204,7 +204,7 @@ val compute_fixdecls_data :
            ?data:Constrintern.internalization_env ->
            Syntax.program_info list ->
            Constrintern.internalization_env *
-           Equations_common.rel_declaration list * (Sorts.relevance * EConstr.t) list
+           Equations_common.rel_declaration list * (ERelevance.t * EConstr.t) list
 
 val wf_fix_constr :
   Environ.env ->

src/depelim.ml

@@ -127,7 +127,7 @@ let annot_of_context ctx =
 let depcase ~poly ((mind, i as ind), u) =
   let indid = Nametab.basename_of_global (GlobRef.IndRef ind) in
   let mindb, oneind = Global.lookup_inductive ind in
-  let relevance = oneind.mind_relevance in
+  let relevance = ERelevance.make oneind.mind_relevance in
   let indna x = make_annot x relevance in
   let ctx = oneind.mind_arity_ctxt in
   let nparams = mindb.mind_nparams in
@@ -143,7 +143,7 @@ let depcase ~poly ((mind, i as ind), u) =
   let nconstrs = Array.length oneind.mind_nf_lc in
   let mkbody i (ctx, ty) =
     let args = Context.Rel.instance mkRel 0 ctx in
-    annot_of_context ctx, mkApp (mkRel (1 + nconstrs + List.length ctx - i), args)
+    annot_of_context (EConstr.of_rel_context ctx), mkApp (mkRel (1 + nconstrs + List.length ctx - i), args)
   in
   let bodies = Array.mapi mkbody oneind.mind_nf_lc in
   let branches =
@@ -185,7 +185,7 @@ let depcase ~poly ((mind, i as ind), u) =
     it_mkLambda_or_LetIn case
       (make_assum (indna xid) (lift len indapp)
         :: ((Array.rev_to_list branches)
-            @ (make_assum (make_annot (Name (Id.of_string "P")) (Retyping.relevance_of_sort !evd s)) pred :: ctx)))
+            @ (make_assum (make_annot (Name (Id.of_string "P")) (Retyping.relevance_of_sort s)) pred :: ctx)))
   in
   let () = evd := Evd.minimize_universes !evd in
   let univs = Evd.univ_entry ~poly !evd in

src/eqdec.ml

@@ -68,7 +68,7 @@ let inductive_info sigma ((mind, _ as ind),u) =
     in
     let case c pred brs =
       let ci = make_case_info (Global.env ()) (mind,i) Constr.RegularStyle in
-      mkCase (EConstr.contract_case env sigma (ci, (pred, Sorts.Relevant), Constr.NoInvert, c, brs))
+      mkCase (EConstr.contract_case env sigma (ci, (pred, ERelevance.relevant), Constr.NoInvert, c, brs))
       (* TODO relevance / case inversion *)
     in
       { ind_name = indname;
@@ -109,8 +109,8 @@ let derive_eq_dec ~pm env sigma ~poly ind =
       mkApp (dec_eq evdref, [| indapp |])
     in
     let app = 
-      let xname = Context.nameR (Id.of_string "x") in
-      let yname = Context.nameR (Id.of_string "y") in
+      let xname = nameR (Id.of_string "x") in
+      let yname = nameR (Id.of_string "y") in
       mkProd (xname, indapp,
             mkProd (yname, lift 1 indapp,
                 mkApp (lift 2 app, [| mkRel 2; mkRel 1 |])))

src/equations.ml

@@ -199,10 +199,7 @@ let define_by_eqs ~pm ~poly ~program_mode ~tactic ~open_proof opts eqs nt =
     progs.(i) <- Some (p, compiled_info);
     if CArray.for_all (fun x -> not (Option.is_empty x)) progs then
       (let progs = Array.map_to_list (fun x -> Option.get x) progs in
-       let is_relevant (rel, _) = match Evarutil.nf_relevance !evd rel with
-       | Sorts.Irrelevant -> false
-       | Sorts.Relevant | Sorts.RelevanceVar _ -> true
-       in
+       let is_relevant (rel, _) = not @@ ERelevance.is_irrelevant !evd rel in
        let relevant = List.for_all is_relevant fixprots in
        let rec_info = compute_rec_type [] (List.map (fun (x, y) -> x.program_info) progs) in
        List.iter (Metasyntax.add_notation_interpretation ~local:false (Global.env ())) nt;

src/equations_common.mli

@@ -344,19 +344,19 @@ val move_after_deps : Names.Id.t -> constr -> unit Proofview.tactic
 
 val extended_rel_vect : int -> rel_context -> constr array
 val extended_rel_list : int -> rel_context -> constr list
-val to_tuple : rel_declaration -> Names.Name.t Context.binder_annot * constr option * constr
-val to_named_tuple : named_declaration -> Names.Id.t Context.binder_annot * constr option * constr
-val of_tuple : Names.Name.t Context.binder_annot * constr option * constr -> rel_declaration
-val of_named_tuple : Names.Id.t Context.binder_annot * constr option * constr -> named_declaration
+val to_tuple : rel_declaration -> Names.Name.t binder_annot * constr option * constr
+val to_named_tuple : named_declaration -> Names.Id.t binder_annot * constr option * constr
+val of_tuple : Names.Name.t binder_annot * constr option * constr -> rel_declaration
+val of_named_tuple : Names.Id.t binder_annot * constr option * constr -> named_declaration
 
 val get_type : rel_declaration -> constr
 val get_name : rel_declaration -> Names.Name.t
-val get_annot : rel_declaration -> Names.Name.t Context.binder_annot
+val get_annot : rel_declaration -> Names.Name.t binder_annot
 val get_value : rel_declaration -> constr option
-val make_assum : Names.Name.t Context.binder_annot -> constr -> rel_declaration
-val make_def : Names.Name.t Context.binder_annot -> constr option -> constr -> rel_declaration
-val make_named_def : Names.Id.t Context.binder_annot -> constr option -> constr -> named_declaration
-val to_context : (Names.Name.t Context.binder_annot * constr option * constr) list -> rel_context
+val make_assum : Names.Name.t binder_annot -> constr -> rel_declaration
+val make_def : Names.Name.t binder_annot -> constr option -> constr -> rel_declaration
+val make_named_def : Names.Id.t binder_annot -> constr option -> constr -> named_declaration
+val to_context : (Names.Name.t binder_annot * constr option * constr) list -> rel_context
 
 val named_of_rel_context : ?keeplets:bool -> (unit -> Names.Id.t) -> rel_context -> EConstr.t list * constr list * named_context
 val rel_of_named_context : Evd.evar_map -> named_context -> rel_context * Names.Id.t list

src/extra_tactics.ml

@@ -9,7 +9,7 @@ let decompose_app h h' c =
   Proofview.Goal.enter begin fun gl ->
     let f, args = EConstr.decompose_app (Proofview.Goal.sigma gl) c in
     let fty = Tacmach.pf_hnf_type_of gl f in
-    let flam = mkLambda (Context.nameR (Id.of_string "f"), fty, mkApp (mkRel 1, args)) in
+    let flam = mkLambda (EConstr.nameR (Id.of_string "f"), fty, mkApp (mkRel 1, args)) in
       (Proofview.tclTHEN (letin_tac None (Name h) f None allHyps)
          (letin_tac None (Name h') flam None allHyps)) end
 

src/noconf.ml

@@ -44,7 +44,7 @@ let mkcase env sigma c ty constrs =
       it_mkLambda_or_LetIn res args)
       oneind.mind_consnames oneind.mind_nf_lc
   in
-    make_case_or_project env sigma indty ci (ty, Sorts.Relevant) c brs
+    make_case_or_project env sigma indty ci (ty, ERelevance.relevant) c brs
 
 let mk_eq env env' evd args args' =
   let _, _, make = Sigma_types.telescope env evd args in
@@ -68,7 +68,7 @@ let derive_no_confusion ~pm env sigma0 ~poly (ind,u as indu) =
   let paramsvect, rest = Array.chop params argsvect in
   let argr, argty, x, ctx, argsctx =
     if Array.length rest = 0 then
-      oneind.mind_relevance, mkApp (mkIndU indu, argsvect), mkRel 1, ctx, []
+      ERelevance.make oneind.mind_relevance, mkApp (mkIndU indu, argsvect), mkRel 1, ctx, []
     else
       let evm, pred, pars, indty, valsig, ctx, lenargs, idx =
         Sigma_types.build_sig_of_ind env !evd indu
@@ -79,7 +79,7 @@ let derive_no_confusion ~pm env sigma0 ~poly (ind,u as indu) =
       let _, pred' = Term.decompose_lambda_n (List.length pars) (EConstr.to_constr !evd pred) in
       let indty = mkApp (sigma, [|idx; of_constr pred'|]) in
       (* sigma is not sort poly (at least for now) *)
-      Sorts.Relevant, nf_betaiotazeta env !evd indty, mkProj (Lazy.force coq_pr2, Relevant, mkRel 1), pars, (List.firstn lenargs ctx)
+      ERelevance.relevant, nf_betaiotazeta env !evd indty, mkProj (Lazy.force coq_pr2, ERelevance.relevant, mkRel 1), pars, (List.firstn lenargs ctx)
   in
   let tru = get_efresh logic_top evd in
   let fls = get_efresh logic_bot evd in

src/principles.ml

@@ -135,7 +135,7 @@ let clean_rec_calls sigma (hyps, c) =
   let elems = List.sort (fun x y -> Int.compare (snd x) (snd y)) (CMap.bindings hyps) in
   let (size, ctx) =
     List.fold_left (fun (n, acc) (ty, _) ->
-    (succ n, LocalAssum (nameR (Id.of_string "Hind"), EConstr.Vars.lift n (EConstr.of_constr ty)) :: acc))
+    (succ n, LocalAssum (EConstr.nameR (Id.of_string "Hind"), EConstr.Vars.lift n (EConstr.of_constr ty)) :: acc))
     (0, []) elems
   in
   (ctx, size, EConstr.Vars.lift size (EConstr.of_constr c))
@@ -1281,7 +1281,7 @@ let declare_funelim ~pm info env evd is_rec protos progs
     with Type_errors.TypeError (env, tyerr) ->
       CErrors.user_err Pp.(str"Error while typechecking elimination principle type: " ++
                            Himsg.explain_pretype_error env !evd
-                             (Pretype_errors.TypingError (Type_errors.map_ptype_error EConstr.of_constr tyerr)))
+                             (Pretype_errors.TypingError (Pretype_errors.of_type_error tyerr)))
   in
   let newty = collapse_term_qualities (Evd.evar_universe_context !evd) (EConstr.to_constr !evd newty) in 
   let cinfo = Declare.CInfo.make ~name:(Nameops.add_suffix id "_elim") ~typ:newty () in
@@ -1354,7 +1354,7 @@ let declare_funind ~pm info alias env evd is_rec protos progs
       | Type_errors.TypeError (env, tyerr) ->
         CErrors.user_err Pp.(str"Functional elimination principle could not be proved automatically: " ++
                              Himsg.explain_pretype_error env !evd
-                               (Pretype_errors.TypingError (Type_errors.map_ptype_error EConstr.of_constr tyerr)))
+                               (Pretype_errors.TypingError (Pretype_errors.of_type_error tyerr)))
       | Pretype_errors.PretypeError (env, sigma, tyerr) ->
         CErrors.user_err Pp.(str"Functional elimination principle could not be proved automatically: " ++
                              Himsg.explain_pretype_error env sigma tyerr)
@@ -1416,7 +1416,7 @@ let declare_funind ~pm info alias env evd is_rec protos progs
   with Type_errors.TypeError (env, tyerr) ->
     CErrors.user_err Pp.(str"Functional induction principle could not be proved automatically: " ++
                          Himsg.explain_pretype_error env !evd
-                           (Pretype_errors.TypingError (Type_errors.map_ptype_error EConstr.of_constr tyerr)))
+                           (Pretype_errors.TypingError (Pretype_errors.of_type_error tyerr)))
      | e when CErrors.noncritical e ->
        Feedback.msg_warning Pp.(str "Functional induction principle could not be proved automatically: " ++ fnl () ++
                                 CErrors.print e);

src/principles_proofs.ml

@@ -143,7 +143,7 @@ let mutual_fix li l =
       let ctxs = List.map (fun evi -> EConstr.Unsafe.to_named_context @@
                             Evd.evar_context evi) infos in
       let fst, rest = List.sep_last ctxs in
-      if List.for_all (fun y -> Context.Named.equal Constr.equal fst y) rest then
+      if List.for_all (fun y -> Context.Named.equal Sorts.relevance_equal Constr.equal fst y) rest then
         Environ.push_named_context fst env
       else env
     in
@@ -179,7 +179,7 @@ let mutual_fix li l =
          if try ignore (Context.Named.lookup f sign); true with Not_found -> false then
            CErrors.user_err
                     (str "Name " ++ pr_id f ++ str " already used in the environment");
-         mk_sign (LocalAssum (make_annot f r, EConstr.to_constr sigma ar) :: sign) oth
+         mk_sign (LocalAssum (make_annot f (ERelevance.kind sigma r), EConstr.to_constr sigma ar) :: sign) oth
     in
     let sign = mk_sign (Environ.named_context env) all in
     let idx = Array.map_of_list pred l in

src/sigma_types.ml

@@ -49,12 +49,12 @@ let constrs_of_coq_sigma env evd t alias =
 	(match kind !evd ty with
           | Prod (n, b, t) ->
             (* sigma is not sort poly (at least for now) *)
-            let p1 = mkProj (Lazy.force coq_pr1, Relevant, proj) in
-            let p2 = mkProj (Lazy.force coq_pr2, Relevant, proj) in
+            let p1 = mkProj (Lazy.force coq_pr1, ERelevance.relevant, proj) in
+            let p2 = mkProj (Lazy.force coq_pr2, ERelevance.relevant, proj) in
 	    (n, args.(2), p1, args.(0)) ::
               aux (push_rel (of_tuple (n, None, b)) env) p2 args.(3) t
 	| _ -> raise (Invalid_argument "constrs_of_coq_sigma"))
-    | _ -> [(Context.anonR, c, proj, ty)]
+    | _ -> [(anonR, c, proj, ty)]
   in aux env alias t (Retyping.get_type_of env !evd t)
 
 let decompose_coq_sigma env sigma t = 
@@ -166,8 +166,8 @@ let telescope env evd = function
 	(fun pred d (prev, k, subst) ->
           let (n, b, t) = to_tuple d in
           (* sigma is not sort poly (at least for now) *)
-          let proj1 = mkProj (Lazy.force coq_pr1, Relevant, prev) in
-          let proj2 = mkProj (Lazy.force coq_pr2, Relevant, prev) in
+          let proj1 = mkProj (Lazy.force coq_pr1, ERelevance.relevant, prev) in
+          let proj2 = mkProj (Lazy.force coq_pr2, ERelevance.relevant, prev) in
 	    (Vars.lift 1 proj2, succ k, of_tuple (n, Some proj1, Vars.liftn 1 k t) :: subst))
 	(List.rev tys) tl (mkRel 1, 1, [])
       in ty, (of_tuple (n, Some last, Vars.liftn 1 len t) :: subst), constr
@@ -823,8 +823,8 @@ let curry_concl env sigma na dom codom =
     if last then (acc :: terms, acc)
     else
       (* sigma is not sort poly (at least for now) *)
-      let term = mkProj (Lazy.force coq_pr1, Relevant, acc) in
-      let acc = mkProj (Lazy.force coq_pr2, Relevant, acc) in
+      let term = mkProj (Lazy.force coq_pr1, ERelevance.relevant, acc) in
+      let acc = mkProj (Lazy.force coq_pr2, ERelevance.relevant, acc) in
       (term :: terms, acc)
   in
   let terms, acc =

src/sigma_types.mli

@@ -6,7 +6,6 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-open Context
 open EConstr
 
 val mkAppG :

src/simplify.ml

@@ -1,5 +1,4 @@
 open Pp
-open Context
 open EConstr
 open Equations_common
 
@@ -230,7 +229,7 @@ let check_typed ~where ?name env evd c =
       anomaly Pp.(str where ++ spc () ++
         str "Equations build an ill-typed term: " ++ Printer.pr_econstr_env env evd c ++
         Himsg.explain_pretype_error env evd
-          (Pretype_errors.TypingError (Type_errors.map_ptype_error EConstr.of_constr tyerr)))
+          (Pretype_errors.TypingError (Pretype_errors.of_type_error tyerr)))
     | Pretype_errors.PretypeError (env, evd, tyerr) ->
         anomaly Pp.(str where ++ spc () ++
         str "Equations build an ill-typed term: " ++ Printer.pr_econstr_env env evd c ++
@@ -317,7 +316,7 @@ let build_term (env : Environ.env) (evd : Evd.evar_map ref) (gl : goal) (ngl : g
     with Type_errors.TypeError (env, tyerr) ->
       anomaly Pp.(str "Equations build an ill-typed term: " ++ Printer.pr_econstr_env env !evd c ++ 
         Himsg.explain_pretype_error env !evd
-          (Pretype_errors.TypingError (Type_errors.map_ptype_error EConstr.of_constr tyerr)))
+          (Pretype_errors.TypingError (Pretype_errors.of_type_error tyerr)))
     | Pretype_errors.PretypeError (env, evd, tyerr) ->
         anomaly Pp.(str "Equations build an ill-typed term: " ++ Printer.pr_econstr_env env evd c ++ 
             Himsg.explain_pretype_error env evd tyerr)

src/splitting.ml

@@ -156,7 +156,7 @@ let where_id w = w.where_program.program_info.program_id
 
 let where_context wheres =
   List.map (fun ({where_program; where_type } as w) ->
-             make_def (Context.nameR (where_id w)) (Some (where_term w)) where_type) wheres
+             make_def (nameR (where_id w)) (Some (where_term w)) where_type) wheres
 
 let where_program_type w =
   program_type w.where_program
@@ -371,7 +371,7 @@ let define_mutual_nested env evd get_prog progs =
       in
       let after = (nested - 1) - before in
       let fixb = (Array.make 1 idx, 0) in
-      let fixna = Array.make 1 (make_annot (Name p.program_id) (Retyping.relevance_of_sort !evd (ESorts.make p.program_sort))) in
+      let fixna = Array.make 1 (make_annot (Name p.program_id) (Retyping.relevance_of_sort (ESorts.make p.program_sort))) in
       let fixty = Array.make 1 (Syntax.program_type p) in
       (* Apply to itself *)
       let beforeargs = Termops.rel_list (signlen + 1) before in
@@ -470,7 +470,7 @@ let check_typed ~where ?name env evd c =
       anomaly Pp.(str where ++ spc () ++
         str "Equations build an ill-typed term: " ++ Printer.pr_econstr_env env evd c ++
         Himsg.explain_pretype_error env evd
-          (Pretype_errors.TypingError (Type_errors.map_ptype_error EConstr.of_constr tyerr)))
+          (Pretype_errors.TypingError (Pretype_errors.of_type_error tyerr)))
     | Pretype_errors.PretypeError (env, evd, tyerr) ->
         anomaly Pp.(str where ++ spc () ++
         str "Equations build an ill-typed term: " ++ Printer.pr_econstr_env env evd c ++