Merge pull request #114 from SkySkimmer/sort-poly

Adapt to coq/coq#17836 (sort poly)
coq-community · Nov 6, 2023 · 2d25c4c · 2d25c4c
2 parents 1f3d001 + a28769f
commit 2d25c4c
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 11 deletions.
diff --git a/src/debug.ml b/src/debug.ml
@@ -195,7 +195,7 @@ let debug_mutual_inductive_entry =
       match entry.mind_entry_universes with
       | Monomorphic_ind_entry | Template_ind_entry _ -> mt ()
       | Polymorphic_ind_entry ux ->
-         Univ.pr_universe_context UnivNames.pr_with_global_universes ux
+         UVars.pr_universe_context Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes ux
     in
     let mind_entry_cumul_pp = bool (Option.has_some entry.mind_entry_variance) in
     let mind_entry_private_pp =

diff --git a/src/declare_translation.ml b/src/declare_translation.ml
@@ -91,13 +91,13 @@ let declare_abstraction ?(opaque = false) ?(continuation = default_continuation)
     match EConstr.kind !evdr a with
       | Const cte when
           let cte = (fst cte, EInstance.kind !evdr (snd cte)) in
-          (try ignore (Relations.get_constant arity (Univ.out_punivs cte)); false with Not_found -> true)
+          (try ignore (Relations.get_constant arity (UVars.out_punivs cte)); false with Not_found -> true)
         ->
         Declare.Hook.(make (fun { dref ; _ } ->
             if !ongoing_translation then error (Pp.str "Please use the 'Debug.Done' command to end proof obligations generated by the parametricity tactic.");
             Pp.(Flags.if_verbose msg_info (str (Printf.sprintf "'%s' is now a registered translation." (Names.Id.to_string name))));
             let cte = (fst cte, EInstance.kind !evdr (snd cte)) in
-            Relations.declare_relation arity (Names.GlobRef.ConstRef (Univ.out_punivs cte)) dref;
+            Relations.declare_relation arity (Names.GlobRef.ConstRef (UVars.out_punivs cte)) dref;
             continuation ()))
       | _ -> Declare.Hook.(make (fun _ -> continuation ()))
   in
@@ -112,7 +112,7 @@ let declare_inductive name ?(continuation = default_continuation) arity evd env
   debug_evar_map [`Inductive] "evar_map inductive " env !evd;
   let size = Declarations.(Array.length mut_body.mind_packets) in
   let mut_ind_R = DeclareInd.declare_mutual_inductive_with_eliminations translation_entry
-                  (Monomorphic_entry Univ.ContextSet.empty, Names.Id.Map.empty) [] in
+                  (Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders) [] in
   for k = 0 to size-1 do
     Relations.declare_inductive_relation arity (mut_ind, k) (mut_ind_R, k)
   done;
@@ -239,7 +239,7 @@ and declare_module ?(continuation = ignore) ?name arity mb  =
        let env = Global.env () in
        let evd = Evd.from_env env in
        let evd, ucst =
-          Evd.(with_context_set univ_rigid evd (UnivGen.fresh_constant_instance env cst))
+          Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_constant_instance env cst))
        in
        let evdr = ref evd in
        ignore(declare_realizer ~continuation arity evdr env None (mkConstU (fst ucst, EInstance.make (snd ucst))))
@@ -258,7 +258,7 @@ and declare_module ?(continuation = ignore) ?name arity mb  =
        let env = Global.env () in
        let evd = Evd.from_env env in
        let evd, ucst =
-          Evd.(with_context_set univ_rigid evd (UnivGen.fresh_constant_instance env cst))
+          Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_constant_instance env cst))
        in
        let c = mkConstU (fst ucst, EInstance.make (snd ucst)) in
        let evdr = ref evd in
@@ -282,7 +282,7 @@ and declare_module ?(continuation = ignore) ?name arity mb  =
          continuation ()
        else begin
          let evd, pind =
-            Evd.(with_context_set univ_rigid !evdr (UnivGen.fresh_inductive_instance env ind))
+            Evd.(with_sort_context_set univ_rigid !evdr (UnivGen.fresh_inductive_instance env ind))
          in
          evdr := evd;
          debug_string [`Module] (Printf.sprintf "inductive field: '%s'." (Names.Label.to_string lab));
@@ -351,7 +351,7 @@ let command_constant ?(continuation = default_continuation) ~fullname arity cons
   let scope = Locality.(Global ImportDefaultBehavior) in
   let kind = Decls.(IsDefinition Definition) in
   let evd, pconst =
-    Evd.(with_context_set univ_rigid evd (UnivGen.fresh_constant_instance env constant))
+    Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_constant_instance env constant))
   in
   let constr = mkConstU (fst pconst, EInstance.make @@ snd pconst) in
   declare_abstraction ~continuation ~opaque ~poly ~scope ~kind arity (ref evd) env constr name
@@ -360,7 +360,7 @@ let command_inductive ?(continuation = default_continuation) ~fullname arity ind
   let env = Global.env () in
   let evd = Evd.from_env env in
   let evd, pind =
-    Evd.(with_context_set univ_rigid evd (UnivGen.fresh_inductive_instance env inductive))
+    Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_inductive_instance env inductive))
   in
   let name = match names with
       | None ->

diff --git a/src/parametricity.ml b/src/parametricity.ml
@@ -426,8 +426,10 @@ and translate order evd env (t : constr) : constr =
     | CoFix _ ->
         translate_cofix order evd env t
 
-    | Proj (p, c) ->
-        mkProj (Projection.map (fun cte -> Names.MutInd.make1 (Names.Constant.canonical (Globnames.destConstRef (Relations.get_constant order (Names.Constant.make1 (Names.MutInd.canonical cte)))))) p, translate order evd env c)
+    | Proj (p, r, c) ->
+      mkProj (Projection.map (fun cte -> Names.MutInd.make1 (Names.Constant.canonical (Globnames.destConstRef (Relations.get_constant order (Names.Constant.make1 (Names.MutInd.canonical cte)))))) p,
+              r,
+              translate order evd env c)
 
     | _ -> not_implemented ~reason:"trapfall" env !evd t
  in