aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.ml13
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/cbv.ml1
-rw-r--r--pretyping/coercion.ml1
-rw-r--r--pretyping/detyping.ml7
-rw-r--r--pretyping/evarconv.ml6
-rw-r--r--pretyping/glob_ops.ml5
-rw-r--r--pretyping/glob_term.ml2
-rw-r--r--pretyping/inductiveops.ml4
-rw-r--r--pretyping/pretyping.ml7
-rw-r--r--pretyping/pretyping.mli6
-rw-r--r--pretyping/program.ml3
-rw-r--r--pretyping/recordops.ml4
-rw-r--r--pretyping/reductionops.ml41
-rw-r--r--pretyping/tacred.ml10
-rw-r--r--pretyping/typeclasses.ml13
-rw-r--r--pretyping/typing.ml22
-rw-r--r--pretyping/typing.mli3
-rw-r--r--pretyping/unification.ml13
19 files changed, 74 insertions, 89 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 36f35a67c3..59ca418a39 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -11,7 +11,6 @@
(*i*)
open Names
open Globnames
-open Term
open Constr
open Context
open Environ
@@ -78,14 +77,14 @@ let rename_type ty ref =
let rec rename_type_aux c = function
| [] -> c
| rename :: rest as renamings ->
- match kind_of_type c with
- | ProdType (old, s, t) ->
+ match Constr.kind c with
+ | Prod (old, s, t) ->
mkProd (name_override old rename, s, rename_type_aux t rest)
- | LetInType(old, s, b, t) ->
+ | LetIn (old, s, b, t) ->
mkLetIn (old ,s, b, rename_type_aux t renamings)
- | CastType (t,_) -> rename_type_aux t renamings
- | SortType _ -> c
- | AtomicType _ -> c in
+ | Cast (t,_, _) -> rename_type_aux t renamings
+ | _ -> c
+ in
try rename_type_aux ty (arguments_names ref)
with Not_found -> ty
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index cbd04a76ad..29d6726262 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2164,7 +2164,7 @@ let constr_of_pat env sigma arsign pat avoid =
let IndType (indf, _) =
try find_rectype env sigma (lift (-(List.length realargs)) ty)
with Not_found -> error_case_not_inductive env sigma
- {uj_val = ty; uj_type = Typing.unsafe_type_of env sigma ty}
+ {uj_val = ty; uj_type = Retyping.get_type_of env sigma ty}
in
let (ind,u), params = dest_ind_family indf in
let params = List.map EConstr.of_constr params in
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2b7ccbbcad..11c97221ec 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -196,7 +196,6 @@ let cofixp_reducible flgs _ stk =
let get_debug_cbv = Goptions.declare_bool_option_and_ref
~depr:false
~value:false
- ~name:"cbv visited constants display"
~key:["Debug";"Cbv"]
(* Reduction of primitives *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3c7f9a8f00..c4aa3479bf 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -36,7 +36,6 @@ open Globnames
let get_use_typeclasses_for_conversion =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"use typeclass resolution during conversion"
~key:["Typeclass"; "Resolution"; "For"; "Conversion"]
~value:true
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b042437a22..83078660c5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -228,7 +228,6 @@ let force_wildcard () = !wildcard_value
let () = declare_bool_option
{ optdepr = false;
- optname = "forced wildcard";
optkey = ["Printing";"Wildcard"];
optread = force_wildcard;
optwrite = (:=) wildcard_value }
@@ -237,7 +236,6 @@ let fast_name_generation = ref false
let () = declare_bool_option {
optdepr = false;
- optname = "fast bound name generation algorithm";
optkey = ["Fast";"Name";"Printing"];
optread = (fun () -> !fast_name_generation);
optwrite = (:=) fast_name_generation;
@@ -248,7 +246,6 @@ let synthetize_type () = !synth_type_value
let () = declare_bool_option
{ optdepr = false;
- optname = "pattern matching return type synthesizability";
optkey = ["Printing";"Synth"];
optread = synthetize_type;
optwrite = (:=) synth_type_value }
@@ -258,7 +255,6 @@ let reverse_matching () = !reverse_matching_value
let () = declare_bool_option
{ optdepr = false;
- optname = "pattern-matching reversibility";
optkey = ["Printing";"Matching"];
optread = reverse_matching;
optwrite = (:=) reverse_matching_value }
@@ -268,7 +264,6 @@ let print_primproj_params () = !print_primproj_params_value
let () = declare_bool_option
{ optdepr = false;
- optname = "printing of primitive projection parameters";
optkey = ["Printing";"Primitive";"Projection";"Parameters"];
optread = print_primproj_params;
optwrite = (:=) print_primproj_params_value }
@@ -348,7 +343,6 @@ let print_factorize_match_patterns = ref true
let () =
declare_bool_option
{ optdepr = false;
- optname = "factorization of \"match\" patterns in printing";
optkey = ["Printing";"Factorizable";"Match";"Patterns"];
optread = (fun () -> !print_factorize_match_patterns);
optwrite = (fun b -> print_factorize_match_patterns := b) }
@@ -358,7 +352,6 @@ let print_allow_match_default_clause = ref true
let () =
declare_bool_option
{ optdepr = false;
- optname = "possible use of \"match\" default pattern in printing";
optkey = ["Printing";"Allow";"Match";"Default";"Clause"];
optread = (fun () -> !print_allow_match_default_clause);
optwrite = (fun b -> print_allow_match_default_clause := b) }
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3bd52088c7..c67019c7ac 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -50,8 +50,6 @@ let default_flags env =
let debug_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print states sent to Evarconv unification";
optkey = ["Debug";"Unification"];
optread = (fun () -> !debug_unification);
optwrite = (fun a -> debug_unification:=a);
@@ -60,8 +58,6 @@ let () = Goptions.(declare_bool_option {
let debug_ho_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print higher-order unification debug information";
optkey = ["Debug";"HO";"Unification"];
optread = (fun () -> !debug_ho_unification);
optwrite = (fun a -> debug_ho_unification:=a);
@@ -269,7 +265,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
let sk2 = Stack.append_app args sk2 in
lookup_canonical_conversion (proji, Const_cs c2), sk2
| _ ->
- let (c2, _) = Termops.global_of_constr sigma t2 in
+ let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in
lookup_canonical_conversion (proji, Const_cs c2),sk2
with Not_found ->
let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 02c2fc4a13..0969b3cc03 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -68,8 +68,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with
let binding_kind_eq bk1 bk2 = match bk1, bk2 with
| Explicit, Explicit -> true
- | Implicit, Implicit -> true
- | (Explicit | Implicit), _ -> false
+ | NonMaxImplicit, NonMaxImplicit -> true
+ | MaxImplicit, MaxImplicit -> true
+ | (Explicit | NonMaxImplicit | MaxImplicit), _ -> false
let case_style_eq s1 s2 = let open Constr in match s1, s2 with
| LetStyle, LetStyle -> true
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 44323441b6..485a19421d 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -65,7 +65,7 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t
type cases_pattern = [ `any ] cases_pattern_g
-type binding_kind = Explicit | Implicit
+type binding_kind = Explicit | MaxImplicit | NonMaxImplicit
(** Representation of an internalized (or in other words globalized) term. *)
type 'a glob_constr_r =
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 36b405e981..816a8c4703 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -28,14 +28,14 @@ open Context.Rel.Declaration
let type_of_inductive env (ind,u) =
let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- Typeops.check_hyps_inclusion env mkInd ind mib.mind_hyps;
+ Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
Inductive.type_of_inductive env (specif,u)
(* Return type as quoted by the user *)
let type_of_constructor env (cstr,u) =
let (mib,_ as specif) =
Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- Typeops.check_hyps_inclusion env mkConstruct cstr mib.mind_hyps;
+ Typeops.check_hyps_inclusion env (GlobRef.ConstructRef cstr) mib.mind_hyps;
Inductive.type_of_constructor (cstr,u) specif
(* Return constructor types in user form *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bf61d44a10..ac1a4e88ef 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -47,7 +47,7 @@ open Evarconv
module NamedDecl = Context.Named.Declaration
-type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
+type typing_constraint = UnknownIfTermOrType | IsType | OfType of types | WithoutTypeConstraint
let (!!) env = GlobEnv.env env
@@ -125,7 +125,6 @@ let esearch_guard ?loc env sigma indexes fix =
let is_strict_universe_declarations =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"strict universe declaration"
~key:["Strict";"Universe";"Declaration"]
~value:true
@@ -446,7 +445,7 @@ let pretype_ref ?loc sigma env ref us =
Pretype_errors.error_var_not_found ?loc !!env sigma id)
| ref ->
let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in
- let ty = unsafe_type_of !!env sigma c in
+ let sigma, ty = type_of !!env sigma c in
sigma, make_judge c ty
let interp_sort ?loc evd : glob_sort -> _ = function
@@ -1290,7 +1289,7 @@ let ise_pretype_gen flags env sigma lvar kind c =
in
let env = GlobEnv.make ~hypnaming env sigma lvar in
let sigma', c', c'_ty = match kind with
- | WithoutTypeConstraint ->
+ | WithoutTypeConstraint | UnknownIfTermOrType ->
let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in
sigma, j.uj_val, j.uj_type
| OfType exptyp ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 18e416596e..ee57f690a1 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -38,7 +38,11 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
val search_guard :
?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array
-type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
+type typing_constraint =
+ | UnknownIfTermOrType (** E.g., unknown if manual implicit arguments allowed *)
+ | IsType (** Necessarily a type *)
+ | OfType of types (** A term of the expected type *)
+ | WithoutTypeConstraint (** A term of unknown expected type *)
type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 1bc31646dd..9c478844aa 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -78,7 +78,6 @@ open Goptions
let () =
declare_bool_option
{ optdepr = false;
- optname = "preferred transparency of Program obligations";
optkey = ["Transparent";"Obligations"];
optread = get_proofs_transparency;
optwrite = set_proofs_transparency; }
@@ -86,7 +85,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "program cases";
optkey = ["Program";"Cases"];
optread = (fun () -> !program_cases);
optwrite = (:=) program_cases }
@@ -94,7 +92,6 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
- optname = "program generalized coercion";
optkey = ["Program";"Generalized";"Coercion"];
optread = (fun () -> !program_generalized_coercion);
optwrite = (:=) program_generalized_coercion }
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 3b918b5396..879c007198 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -189,7 +189,7 @@ let rec cs_pattern_of_constr env t =
let _, params = Inductive.find_rectype env ty in
Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
| Sort s -> Sort_cs (Sorts.family s), None, []
- | _ -> Const_cs (Globnames.global_of_constr t) , None, []
+ | _ -> Const_cs (fst @@ destRef t) , None, []
let warn_projection_no_head_constant =
CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
@@ -234,7 +234,7 @@ let compute_canonical_projections env ~warn (gref,ind) =
((GlobRef.ConstRef proji_sp, (patt, t)),
{ o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
:: acc
- | exception Not_found ->
+ | exception DestKO ->
if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp);
acc
) acc spopt
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4d4fe13983..bfee07e7f0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -32,8 +32,6 @@ exception Elimconst
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Generate weak constraints between Irrelevant universes";
optkey = ["Cumulativity";"Weak";"Constraints"];
optread = (fun () -> not !UState.drop_weak_constraints);
optwrite = (fun a -> UState.drop_weak_constraints:=not a);
@@ -722,32 +720,31 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
| Name.Anonymous -> bd
| Name.Name id ->
let open UnivProblem in
- try
- let (cst_mod,_) = Constant.repr2 reference in
- let cst = Constant.make2 cst_mod (Label.of_id id) in
+ let (cst_mod,_) = Constant.repr2 reference in
+ let cst = Constant.make2 cst_mod (Label.of_id id) in
+ if not (Environ.mem_constant cst env) then bd
+ else
let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in
match constant_opt_value_in env (cst,u) with
| None -> bd
| Some t ->
let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
begin match csts with
- | Some csts ->
- let subst = Set.fold (fun cst acc ->
- let l, r = match cst with
- | ULub (u, v) | UWeak (u, v) -> u, v
- | UEq (u, v) | ULe (u, v) ->
- let get u = Option.get (Universe.level u) in
- get u, get v
- in
- Univ.LMap.add l r acc)
- csts Univ.LMap.empty
- in
- let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
- mkConstU (cst, EInstance.make inst)
- | None -> bd
+ | Some csts ->
+ let subst = Set.fold (fun cst acc ->
+ let l, r = match cst with
+ | ULub (u, v) | UWeak (u, v) -> u, v
+ | UEq (u, v) | ULe (u, v) ->
+ let get u = Option.get (Universe.level u) in
+ get u, get v
+ in
+ Univ.LMap.add l r acc)
+ csts Univ.LMap.empty
+ in
+ let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
+ mkConstU (cst, EInstance.make inst)
+ | None -> bd
end
- with
- | Not_found -> bd
let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
let nbodies = Array.length bodies in
@@ -973,8 +970,6 @@ module CredNative = RedNative(CNativeEntries)
let debug_RAKAM = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print states of the Reductionops abstract machine";
optkey = ["Debug";"RAKAM"];
optread = (fun () -> !debug_RAKAM);
optwrite = (fun a -> debug_RAKAM:=a);
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 10e8cf7e0f..4afed07eda 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1197,7 +1197,7 @@ let abstract_scheme env sigma (locc,a) (c, sigma) =
let pattern_occs loccs_trm = begin fun env sigma c ->
let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in
try
- let _ = Typing.unsafe_type_of env sigma abstr_trm in
+ let sigma, _ = Typing.type_of env sigma abstr_trm in
(sigma, applist(abstr_trm, List.map snd loccs_trm))
with Type_errors.TypeError (env',t) ->
raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
@@ -1311,11 +1311,9 @@ let reduce_to_ref_gen allow_product env sigma ref t =
else
error_cannot_recognize ref
| _ ->
- try
- if GlobRef.equal (fst (global_of_constr sigma c)) ref
- then it_mkProd_or_LetIn t l
- else raise Not_found
- with Not_found ->
+ if isRefX sigma ref c
+ then it_mkProd_or_LetIn t l
+ else
try
let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in
elimrec env t' l
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1541e96635..aa2e96c2d7 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -31,7 +31,6 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
let get_typeclasses_unique_solutions =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"check that typeclasses proof search returns unique solutions"
~key:["Typeclasses";"Unique";"Solutions"]
~value:false
@@ -107,9 +106,9 @@ let class_info env sigma c =
not_a_class env sigma (EConstr.of_constr (printable_constr_of_global c))
let global_class_of_constr env sigma c =
- try let gr, u = Termops.global_of_constr sigma c in
+ try let gr, u = EConstr.destRef sigma c in
GlobRef.Map.find gr !classes, u
- with Not_found -> not_a_class env sigma c
+ with DestKO | Not_found -> not_a_class env sigma c
let dest_class_app env sigma c =
let cl, args = EConstr.decompose_app sigma c in
@@ -125,9 +124,9 @@ let class_of_constr env sigma c =
with e when CErrors.noncritical e -> None
let is_class_constr sigma c =
- try let gr, u = Termops.global_of_constr sigma c in
+ try let gr, u = EConstr.destRef sigma c in
GlobRef.Map.mem gr !classes
- with Not_found -> false
+ with DestKO | Not_found -> false
let rec is_class_type evd c =
let c, _ = Termops.decompose_app_vect evd c in
@@ -140,9 +139,9 @@ let is_class_evar evd evi =
is_class_type evd evi.Evd.evar_concl
let is_class_constr sigma c =
- try let gr, u = Termops.global_of_constr sigma c in
+ try let gr, u = EConstr.destRef sigma c in
GlobRef.Map.mem gr !classes
- with Not_found -> false
+ with DestKO | Not_found -> false
let rec is_maybe_class_type evd c =
let c, _ = Termops.decompose_app_vect evd c in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index a15134f58d..b4c19775a7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -27,6 +27,8 @@ open Arguments_renaming
open Pretype_errors
open Context.Rel.Declaration
+module GR = Names.GlobRef
+
let meta_type evd mv =
let ty =
try Evd.meta_ftype evd mv
@@ -253,6 +255,9 @@ let judge_of_type u =
let judge_of_relative env v =
Environ.on_judgment EConstr.of_constr (judge_of_relative env v)
+let type_of_variable env id =
+ EConstr.of_constr (type_of_variable env id)
+
let judge_of_variable env id =
Environ.on_judgment EConstr.of_constr (judge_of_variable env id)
@@ -284,37 +289,36 @@ let judge_of_letin env name defj typj j =
{ uj_val = mkLetIn (make_annot name r, defj.uj_val, typj.utj_val, j.uj_val) ;
uj_type = subst1 defj.uj_val j.uj_type }
-let check_hyps_inclusion env sigma f x hyps =
+let check_hyps_inclusion env sigma x hyps =
let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in
- let f x = EConstr.Unsafe.to_constr (f x) in
- Typeops.check_hyps_inclusion env ~evars f x hyps
+ Typeops.check_hyps_inclusion env ~evars x hyps
let type_of_constant env sigma (c,u) =
let open Declarations in
let cb = Environ.lookup_constant c env in
- let () = check_hyps_inclusion env sigma mkConstU (c,u) cb.const_hyps in
+ let () = check_hyps_inclusion env sigma (GR.ConstRef c) cb.const_hyps in
let u = EInstance.kind sigma u in
let ty, csts = Environ.constant_type env (c,u) in
let sigma = Evd.add_constraints sigma csts in
- sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstRef c)))
+ sigma, (EConstr.of_constr (rename_type ty (GR.ConstRef c)))
let type_of_inductive env sigma (ind,u) =
let open Declarations in
let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+ let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
let u = EInstance.kind sigma u in
let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in
let sigma = Evd.add_constraints sigma csts in
- sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.IndRef ind)))
+ sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind)))
let type_of_constructor env sigma ((ind,_ as ctor),u) =
let open Declarations in
let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+ let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
let u = EInstance.kind sigma u in
let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in
let sigma = Evd.add_constraints sigma csts in
- sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor)))
+ sigma, (EConstr.of_constr (rename_type ty (GR.ConstructRef ctor)))
let judge_of_int env v =
Environ.on_judgment EConstr.of_constr (judge_of_int env v)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1b07b2bb78..fd2dc7c2fc 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -30,6 +30,9 @@ val sort_of : env -> evar_map -> types -> evar_map * Sorts.t
(** Typecheck a term has a given type (assuming the type is OK) *)
val check : env -> evar_map -> constr -> types -> evar_map
+(** Type of a variable. *)
+val type_of_variable : env -> variable -> types
+
(** Returns the instantiated type of a metavariable *)
val meta_type : evar_map -> metavariable -> types
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6486435ca2..5b87603d54 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -46,7 +46,6 @@ module NamedDecl = Context.Named.Declaration
let keyed_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname = "Unification is keyed";
optkey = ["Keyed";"Unification"];
optread = (fun () -> !keyed_unification);
optwrite = (fun a -> keyed_unification:=a);
@@ -57,8 +56,6 @@ let is_keyed_unification () = !keyed_unification
let debug_unification = ref (false)
let () = Goptions.(declare_bool_option {
optdepr = false;
- optname =
- "Print states sent to tactic unification";
optkey = ["Debug";"Tactic";"Unification"];
optread = (fun () -> !debug_unification);
optwrite = (fun a -> debug_unification:=a);
@@ -1274,12 +1271,14 @@ let applyHead env evd n c =
else
match EConstr.kind evd (whd_all env evd cty) with
| Prod (_,c1,c2) ->
- let (evd',evar) =
- Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in
- apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
+ let (evd,evar) =
+ Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1
+ in
+ apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd
| _ -> user_err Pp.(str "Apply_Head_Then")
in
- apprec n c (Typing.unsafe_type_of env evd c) evd
+ let evd, t = Typing.type_of env evd c in
+ apprec n c t evd
let is_mimick_head sigma ts f =
match EConstr.kind sigma f with
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:57:27 +0000