Merge branch 'coq-master'

Author: gares

coq-builtin.elpi

@@ -1015,7 +1015,7 @@ external pred coq.univ.variable.of-term i:term, o:coq.univ.variable.set.
 % crafts a fresh, appropriate, universe instance and possibly unify that
 % term (of the instance it contains) with another one.
 
-% Universes level instance for a universe-polymoprhic constant
+% Universes level instance for a universe-polymorphic constant
 typeabbrev univ-instance (ctype "univ-instance").
 
 

src/coq_elpi_HOAS.ml

@@ -19,13 +19,13 @@ type hole_mapping =
 type uinstanceoption =
   | NoInstance
     (* the elpi command involved has to generate a fresh instance *)
-  | ConcreteInstance of Univ.Instance.t
+  | ConcreteInstance of UVars.Instance.t
     (* a concrete instance was provided, the command will use it *)
   | VarInstance of (FlexibleData.Elpi.t * RawData.term list * inv_rel_key)
     (* a variable was provided, the command will compute the instance to unify with it *)
 
 type universe_decl = (Univ.Level.t list * bool) * (Univ.Constraints.t * bool)
-type universe_decl_cumul = ((Univ.Level.t * Univ.Variance.t option) list  * bool) * (Univ.Constraints.t * bool)
+type universe_decl_cumul = ((Univ.Level.t * UVars.Variance.t option) list  * bool) * (Univ.Constraints.t * bool)
 type universe_decl_option =
   | NotUniversePolymorphic
   | Cumulative of universe_decl_cumul
@@ -45,7 +45,7 @@ type options = {
   universe_decl : universe_decl_option;
   reversible : bool option;
   keepunivs : bool option;
-  redflags : CClosure.RedFlags.reds option;
+  redflags : RedFlags.reds option;
   no_tc: bool option;
 }
 
@@ -114,7 +114,7 @@ val lp2inductive_entry :
   State.t * (Entries.mutual_inductive_entry * Univ.ContextSet.t * UnivNames.universe_binders * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
 
 val inductive_decl2lp :
-  depth:int -> empty coq_context -> constraints -> State.t -> (Names.MutInd.t * Univ.Instance.t * (Declarations.mutual_inductive_body * Declarations.one_inductive_body) * (Glob_term.binding_kind list * Glob_term.binding_kind list list)) ->
+  depth:int -> empty coq_context -> constraints -> State.t -> (Names.MutInd.t * UVars.Instance.t * (Declarations.mutual_inductive_body * Declarations.one_inductive_body) * (Glob_term.binding_kind list * Glob_term.binding_kind list list)) ->
     State.t * term * Conversion.extra_goals
 
 val inductive_entry2lp :
@@ -145,7 +145,7 @@ val opt2unspec : 'a option -> 'a Elpi.Builtin.unspec
 
 val in_elpi_gr : depth:int -> State.t -> Names.GlobRef.t -> term
 val in_elpi_poly_gr : depth:int -> State.t -> Names.GlobRef.t -> term -> term
-val in_elpi_poly_gr_instance : depth:int -> State.t -> Names.GlobRef.t -> Univ.Instance.t -> term
+val in_elpi_poly_gr_instance : depth:int -> State.t -> Names.GlobRef.t -> UVars.Instance.t -> term
 val in_elpi_flex_sort : term -> term
 val in_elpi_sort : depth:int -> state -> Sorts.t -> state * term
 val in_elpi_prod : Name.t -> term -> term -> term
@@ -183,10 +183,10 @@ type primitive_value =
   | Projection of Projection.t
 val primitive_value : primitive_value Conversion.t
 val in_elpi_primitive : depth:int -> state -> primitive_value -> state * term
-val uinstance : Univ.Instance.t Conversion.t
+val uinstance : UVars.Instance.t Conversion.t
 
 val universe_constraint : Univ.univ_constraint Conversion.t
-val universe_variance : (Univ.Level.t * Univ.Variance.t option) Conversion.t
+val universe_variance : (Univ.Level.t * UVars.Variance.t option) Conversion.t
 val universe_decl : universe_decl Conversion.t
 val universe_decl_cumul : universe_decl_cumul Conversion.t
 
@@ -202,10 +202,10 @@ module UnivLevelSet : Elpi.API.Utils.Set.S with type elt = Univ.Level.t
 
 val compute_with_uinstance :
   depth:int -> options -> state ->
-  (state -> 'a -> Univ.Instance.t option -> state * 'c * Univ.Instance.t option) ->
+  (state -> 'a -> UVars.Instance.t option -> state * 'c * UVars.Instance.t option) ->
   'a ->
-  Univ.Instance.t option ->
-    state * 'c * Univ.Instance.t option * Conversion.extra_goals
+  UVars.Instance.t option ->
+    state * 'c * UVars.Instance.t option * Conversion.extra_goals
 
 (* CData relevant for other modules, e.g the one exposing Coq's API *)
 val universe_level_variable : Univ.Level.t Conversion.t
@@ -224,7 +224,7 @@ val name : Name.t Conversion.t
 
 type global_or_pglobal =
   | Global of term option
-  | PGlobal of term option * Univ.Instance.t option
+  | PGlobal of term option * UVars.Instance.t option
   | NotGlobal
   | Var
 val is_global_or_pglobal : depth:int -> term -> global_or_pglobal
@@ -236,7 +236,7 @@ val in_coq_modpath : depth:int -> term -> Names.ModPath.t
 val modpath : Names.ModPath.t Conversion.t
 val modtypath : Names.ModPath.t Conversion.t
 val module_inline_default : Declaremods.inline Conversion.t
-val reduction_flags : CClosure.RedFlags.reds Conversion.t
+val reduction_flags : RedFlags.reds Conversion.t
 
 type module_item =
   | Module of Names.ModPath.t * module_item list
@@ -255,12 +255,12 @@ type record_field_att =
 val record_field_att : record_field_att Conversion.t
 
 val add_constraints : State.t -> UnivProblem.Set.t -> State.t
-val mk_global : State.t -> Names.GlobRef.t -> Univ.Instance.t option ->
-  State.t * EConstr.t * Univ.Instance.t option
-val poly_ctx_size_of_gref : Environ.env -> Names.GlobRef.t -> int
+val mk_global : State.t -> Names.GlobRef.t -> UVars.Instance.t option ->
+  State.t * EConstr.t * UVars.Instance.t option
+val poly_ctx_size_of_gref : Environ.env -> Names.GlobRef.t -> int * int
 val body_of_constant :
-  State.t -> Names.Constant.t -> Univ.Instance.t option ->
-  State.t * EConstr.t option * Univ.Instance.t option
+  State.t -> Names.Constant.t -> UVars.Instance.t option ->
+  State.t * EConstr.t option * UVars.Instance.t option
 
 val grab_global_env : State.t -> State.t
 val grab_global_env_drop_univs_and_sigma : State.t -> State.t
@@ -289,7 +289,7 @@ val solution2evd : Evd.evar_map -> 'a Elpi.API.Data.solution -> Evar.Set.t -> Ev
 val show_coq_engine : ?with_univs:bool -> State.t -> string
 val show_coq_elpi_engine_mapping : State.t -> string
 
-val type_of_global : state -> GlobRef.t -> Univ.Instance.t option -> state * (EConstr.t * Univ.Instance.t)
+val type_of_global : state -> GlobRef.t -> UVars.Instance.t option -> state * (EConstr.t * UVars.Instance.t)
 val minimize_universes : state -> state
 val new_univ_level_variable : ?flexible:bool -> state -> state * (Univ.Level.t * Univ.Universe.t)
 val constraint_eq : Sorts.t -> Sorts.t -> UnivProblem.t

src/coq_elpi_HOAS.mli

@@ -283,7 +283,7 @@ let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fi
   let name, space = sep_last_qualid name in
   let sort = match sort with
     | Some x -> Constrexpr.CSort x
-    | None -> Constrexpr.(CSort (Glob_term.UAnonymous {rigid=true})) in
+    | None -> Constrexpr.(CSort (Glob_term.UAnonymous {rigid=UnivRigid})) in
   let intern_env, params = intern_global_context glob_sign ~intern_env:Constrintern.empty_internalization_env parameters in
   let glob_sign_params = push_glob_ctx params glob_sign in
   let params = List.rev params in
@@ -325,7 +325,7 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform
   let name = Names.Id.of_string name in
   let indexes = match arity with
     | Some x -> x
-    | None -> CAst.make Constrexpr.(CSort (Glob_term.UAnonymous {rigid=true})) in
+    | None -> CAst.make Constrexpr.(CSort (Glob_term.UAnonymous {rigid=UnivRigid})) in
   let intern_env, params = intern_global_context glob_sign ~intern_env:Constrintern.empty_internalization_env parameters in
   let nuparams_given, nuparams =
     match non_uniform_parameters with
@@ -348,7 +348,7 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform
   { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly }
 let intern_indt_decl glob_sign (it : raw_indt_decl) = glob_sign, it
 
-let expr_hole = CAst.make @@ Constrexpr.CHole(None,Namegen.IntroAnonymous)
+let expr_hole = CAst.make @@ Constrexpr.CHole(None)
 
 let raw_context_decl_to_glob_synterp fields =
   let fields = intern_global_context_synterp fields in
@@ -564,7 +564,7 @@ let add_genarg tag pr_raw pr_glob pr_top glob subst interp =
   let wit = Genarg.make0 tag in
   let tag = Geninterp.Val.create tag in
   let () = Genintern.register_intern0 wit glob in
-  let () = Genintern.register_subst0 wit subst in
+  let () = Gensubst.register_subst0 wit subst in
   let () = Geninterp.register_interp0 wit (interp (fun x -> Ftactic.return @@ Geninterp.Val.Dyn (tag, x))) in
   let () = Geninterp.register_val0 wit (Some (Geninterp.Val.Base tag)) in
   Ltac_plugin.Pptactic.declare_extra_genarg_pprule wit pr_raw pr_glob pr_top;