diff options
| -rw-r--r-- | engine/eConstr.ml | 6 | ||||
| -rw-r--r-- | engine/eConstr.mli | 2 | ||||
| -rw-r--r-- | engine/univGen.ml | 7 | ||||
| -rw-r--r-- | engine/univGen.mli | 1 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 2 |
7 files changed, 14 insertions, 10 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index cefffb315e..3385b78958 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -74,6 +74,12 @@ let mkCoFix f = of_kind (CoFix f) let mkProj (p, c) = of_kind (Proj (p, c)) let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2)) +let mkRef (gr,u) = let open GlobRef in match gr with + | ConstRef c -> mkConstU (c,u) + | IndRef ind -> mkIndU (ind,u) + | ConstructRef c -> mkConstructU (c,u) + | VarRef x -> mkVar x + let applist (f, arg) = mkApp (f, Array.of_list arg) let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e27eecc24f..1edc0ee12b 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -122,6 +122,8 @@ val mkFix : (t, t) pfixpoint -> t val mkCoFix : (t, t) pcofixpoint -> t val mkArrow : t -> t -> t +val mkRef : GlobRef.t * EInstance.t -> t + val applist : t * t list -> t val mkProd_or_LetIn : rel_declaration -> t -> t diff --git a/engine/univGen.ml b/engine/univGen.ml index 64789cb808..4cdcfd9730 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -105,12 +105,7 @@ let constr_of_global gr = str " would forget universes.") else c -let constr_of_global_univ (gr,u) = - match gr with - | VarRef id -> mkVar id - | ConstRef sp -> mkConstU (sp,u) - | ConstructRef sp -> mkConstructU (sp,u) - | IndRef sp -> mkIndU (sp,u) +let constr_of_global_univ = mkRef let fresh_global_or_constr_instance env = function | IsConstr c -> c, ContextSet.empty diff --git a/engine/univGen.mli b/engine/univGen.mli index 4cfbb94775..82ec9f3e64 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -63,6 +63,7 @@ val fresh_universe_context_set_instance : ContextSet.t -> val global_of_constr : constr -> GlobRef.t puniverses val constr_of_global_univ : GlobRef.t puniverses -> constr +[@@ocaml.deprecated "Use [Constr.mkRef]"] val extend_context : 'a in_universe_context_set -> ContextSet.t -> 'a in_universe_context_set diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 7e5815acd1..ce12aaeeb0 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -320,7 +320,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = UnivGen.constr_of_global_univ (glob, inst) in + let term = Constr.mkRef (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] diff --git a/tactics/equality.ml b/tactics/equality.ml index 3e3ef78c5d..c4a6b1605d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1792,7 +1792,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = try let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in let u = EInstance.kind sigma u in - let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in + let eq = Constr.mkRef (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match EConstr.kind sigma x, EConstr.kind sigma y with | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> @@ -1843,7 +1843,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in let u = EInstance.kind sigma u in - let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in + let eq = Constr.mkRef (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if EConstr.eq_constr sigma x y then failwith "caught"; diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 9497f2fb03..0ef5d56d4f 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -173,7 +173,7 @@ let do_assumptions kind nl l = let t = replace_vars subst t in let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in let subst' = List.map2 - (fun {CAst.v=id} (c,u) -> (id, UnivGen.constr_of_global_univ (c,u))) + (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) idl refs in subst'@subst, status' && status, next_uctx uctx) |