aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml14
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/coercion.ml4
-rw-r--r--pretyping/constr_matching.ml8
-rw-r--r--pretyping/detyping.ml6
-rw-r--r--pretyping/evarconv.ml12
-rw-r--r--pretyping/evarsolve.ml16
-rw-r--r--pretyping/evarsolve.mli2
-rw-r--r--pretyping/inductiveops.ml4
-rw-r--r--pretyping/inductiveops.mli2
-rw-r--r--pretyping/patternops.ml2
-rw-r--r--pretyping/pretyping.ml8
-rw-r--r--pretyping/retyping.ml126
-rw-r--r--pretyping/retyping.mli16
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--pretyping/typeclasses.ml4
-rw-r--r--pretyping/typing.ml2
-rw-r--r--pretyping/unification.ml32
18 files changed, 137 insertions, 127 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index be72091a9..4dd502106 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1480,7 +1480,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
if not (Flags.is_program_mode ()) && (isRel orig || isVar orig) then
(* Try to compile first using non expanded alias *)
try
- if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
+ if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) (EConstr.of_constr orig))
else just_pop ()
with e when precatchable_exception e ->
(* Try then to compile using expanded alias *)
@@ -1495,7 +1495,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
(* Could be needed in case of a recursive call which requires to
be on a variable for size reasons *)
pb.evdref := sigma;
- if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
+ if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) (EConstr.of_constr orig))
else just_pop ()
@@ -1627,7 +1627,7 @@ let abstract_tycon loc env evdref subst tycon extenv t =
let t = whd_evar !evdref t in match kind_of_term t with
| Rel n when is_local_def (lookup_rel n env) -> t
| Evar ev ->
- let ty = get_type_of env !evdref t in
+ let ty = get_type_of env !evdref (EConstr.of_constr t) in
let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in
let inst =
List.map_i
@@ -1649,7 +1649,7 @@ let abstract_tycon loc env evdref subst tycon extenv t =
| (_, _, u) :: _ -> (* u is in extenv *)
let vl = List.map pi1 good in
let ty =
- let ty = get_type_of env !evdref t in
+ let ty = get_type_of env !evdref (EConstr.of_constr t) in
Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty
in
let ty = lift (-k) (aux x ty) in
@@ -1798,7 +1798,7 @@ let build_inversion_problem loc env sigma tms t =
it = None } } ] in
(* [pb] is the auxiliary pattern-matching serving as skeleton for the
return type of the original problem Xi *)
- let s' = Retyping.get_sort_of env sigma t in
+ let s' = Retyping.get_sort_of env sigma (EConstr.of_constr t) in
let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in
let sigma = Evd.set_leq_sort env sigma s' s in
let evdref = ref sigma in
@@ -2067,7 +2067,7 @@ let constr_of_pat env evdref arsign pat avoid =
let cstr = mkConstructU ci.cs_cstr in
let app = applistc cstr (List.map (lift (List.length sign)) params) in
let app = applistc app args in
- let apptype = Retyping.get_type_of env ( !evdref) app in
+ let apptype = Retyping.get_type_of env ( !evdref) (EConstr.of_constr app) in
let IndType (indf, realargs) = find_rectype env (!evdref) (EConstr.of_constr apptype) in
match alias with
Anonymous ->
@@ -2325,7 +2325,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
(fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg decl ->
let name = RelDecl.get_name decl in
let t = RelDecl.get_type decl in
- let argt = Retyping.get_type_of env !evdref arg in
+ let argt = Retyping.get_type_of env !evdref (EConstr.of_constr arg) in
let eq, refl_arg =
if Reductionops.is_conv env !evdref (EConstr.of_constr argt) (EConstr.of_constr t) then
(mk_eq evdref (lift (nargeqs + slift) argt)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index fd21f5bd1..577f41a7d 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -441,7 +441,7 @@ let cache_coercion (_, c) =
let is, _ = class_info c.coercion_source in
let it, _ = class_info c.coercion_target in
let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in
- let typ = Retyping.get_type_of (Global.env ()) Evd.empty value in
+ let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in
let xf =
{ coe_value = value;
coe_type = typ;
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index b062da1f4..6a7f90463 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -65,7 +65,7 @@ let apply_coercion_args env evd check isproj argl funj =
| h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
match kind_of_term (whd_all env evd (EConstr.of_constr typ)) with
| Prod (_,c1,c2) ->
- if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then
+ if check && not (e_cumul env evdref (Retyping.get_type_of env evd (EConstr.of_constr h)) c1) then
raise NoCoercion;
apply_rec (h::acc) (subst1 h c2) restl
| _ -> anomaly (Pp.str "apply_coercion_args")
@@ -488,7 +488,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
let v2 = Option.map (fun v -> beta_applist evd' (EConstr.of_constr (lift 1 v),[EConstr.of_constr v1])) v in
let t2 = match v2 with
| None -> subst_term evd' (EConstr.of_constr v1) (EConstr.of_constr t2)
- | Some v2 -> Retyping.get_type_of env1 evd' v2 in
+ | Some v2 -> Retyping.get_type_of env1 evd' (EConstr.of_constr v2) in
let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
(evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
| _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 66e690714..1261844a0 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -221,7 +221,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
else (* Might be a projection on the right *)
match kind_of_term c2 with
| Proj (pr, c) when not (Projection.unfolded pr) ->
- (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
+ (try let term = Retyping.expand_projection env sigma pr (EConstr.of_constr c) (Array.map_to_list EConstr.of_constr args2) in
sorec ctx env subst p term
with Retyping.RetypeError _ -> raise PatternMatchingFailure)
| _ -> raise PatternMatchingFailure)
@@ -237,7 +237,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
with Invalid_argument _ -> raise PatternMatchingFailure
else raise PatternMatchingFailure
| _, Proj (pr,c) when not (Projection.unfolded pr) ->
- (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
+ (try let term = Retyping.expand_projection env sigma pr (EConstr.of_constr c) (Array.map_to_list EConstr.of_constr arg2) in
sorec ctx env subst p term
with Retyping.RetypeError _ -> raise PatternMatchingFailure)
| _, _ ->
@@ -249,7 +249,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
raise PatternMatchingFailure
| PApp (c, args), Proj (pr, c2) ->
- (try let term = Retyping.expand_projection env sigma pr c2 [] in
+ (try let term = Retyping.expand_projection env sigma pr (EConstr.of_constr c2) [] in
sorec ctx env subst p term
with Retyping.RetypeError _ -> raise PatternMatchingFailure)
@@ -440,7 +440,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
if partial_app then
try
- let term = Retyping.expand_projection env sigma p c' [] in
+ let term = Retyping.expand_projection env sigma p (EConstr.of_constr c') [] in
aux env term mk_ctx next
with Retyping.RetypeError _ -> next ()
else
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a4d943cfa..e5e778f23 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -501,7 +501,7 @@ let rec detype flags avoid env sigma t =
try
let pb = Environ.lookup_projection p (snd env) in
let body = pb.Declarations.proj_body in
- let ty = Retyping.get_type_of (snd env) sigma c in
+ let ty = Retyping.get_type_of (snd env) sigma (EConstr.of_constr c) in
let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma (EConstr.of_constr ty) in
let body' = strip_lam_assum body in
let body' = subst_instance_constr u body' in
@@ -512,7 +512,7 @@ let rec detype flags avoid env sigma t =
else
if print_primproj_params () then
try
- let c = Retyping.expand_projection (snd env) sigma p c [] in
+ let c = Retyping.expand_projection (snd env) sigma p (EConstr.of_constr c) [] in
detype flags avoid env sigma c
with Retyping.RetypeError _ -> noparams ()
else noparams ()
@@ -689,7 +689,7 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
| BLetIn ->
let c = detype (lax,false) avoid env sigma (Option.get body) in
(* Heuristic: we display the type if in Prop *)
- let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
+ let s = try Retyping.get_sort_family_of (snd env) sigma (EConstr.of_constr ty) with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
let c = if s != InProp then c else
GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in
GLetIn (dl, na', c, r)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f54a57d57..47db71cc6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -165,7 +165,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
let params1, c1, extra_args1 =
match arg with
| Some c -> (* A primitive projection applied to c *)
- let ty = Retyping.get_type_of ~lax:true env sigma c in
+ let ty = Retyping.get_type_of ~lax:true env sigma (EConstr.of_constr c) in
let (i,u), ind_args =
try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty)
with _ -> raise Not_found
@@ -464,7 +464,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
else
let f =
try
- let termM' = Retyping.expand_projection env evd p (EConstr.Unsafe.to_constr c) [] in
+ let termM' = Retyping.expand_projection env evd p c [] in
let apprM', cstsM' =
whd_betaiota_deltazeta_for_iota_state
(fst ts) env evd cstsM (EConstr.of_constr termM',skM)
@@ -643,7 +643,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(* Catch the p.c ~= p c' cases *)
| Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' ->
let res =
- try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p c [])))
+ try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p (EConstr.of_constr c) [])))
with Retyping.RetypeError _ -> None
in
(match res with
@@ -654,7 +654,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') ->
let res =
- try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' c' [])))
+ try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' (EConstr.of_constr c') [])))
with Retyping.RetypeError _ -> None
in
(match res with
@@ -888,7 +888,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
List.fold_left
(fun (i,ks,m,test) b ->
if match n with Some n -> Int.equal m n | None -> false then
- let ty = Retyping.get_type_of env i t2 in
+ let ty = Retyping.get_type_of env i (EConstr.of_constr t2) in
let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in
(i,t2::ks, m-1, test)
else
@@ -1058,7 +1058,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
let id = NamedDecl.get_id decl' in
let t = NamedDecl.get_type decl' in
let evs = ref [] in
- let ty = Retyping.get_type_of env_rhs evd c in
+ let ty = Retyping.get_type_of env_rhs evd (EConstr.of_constr c) in
let filter' = filter_possible_projections evd c ty ctxt args in
(id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl)
| _, _, [] -> []
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 17bb1406e..86ef8f56f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -141,8 +141,8 @@ let recheck_applications conv_algo env evdref t =
match kind_of_term t with
| App (f, args) ->
let () = aux env f in
- let fty = Retyping.get_type_of env !evdref f in
- let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in
+ let fty = Retyping.get_type_of env !evdref (EConstr.of_constr f) in
+ let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref (EConstr.of_constr x)) args in
let rec aux i ty =
if i < Array.length argsty then
match kind_of_term (whd_all env !evdref (EConstr.of_constr ty)) with
@@ -634,7 +634,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in
let id = next_name_away na avoid in
let evd,t_in_sign =
- let s = Retyping.get_sort_of env evd t_in_env in
+ let s = Retyping.get_sort_of env evd (EConstr.of_constr t_in_env) in
let evd,ty_t_in_sign = refresh_universes
~status:univ_flexible (Some false) env evd (mkSort s) in
define_evar_from_virtual_equation define_fun env evd src t_in_env
@@ -653,7 +653,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
(sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
in
let evd,ev2ty_in_sign =
- let s = Retyping.get_sort_of env evd ty_in_env in
+ let s = Retyping.get_sort_of env evd (EConstr.of_constr ty_in_env) in
let evd,ty_t_in_sign = refresh_universes
~status:univ_flexible (Some false) env evd (mkSort s) in
define_evar_from_virtual_equation define_fun env evd src ty_in_env
@@ -1161,7 +1161,7 @@ let check_evar_instance evd evk1 body conv_algo =
(* FIXME: The body might be ill-typed when this is called from w_merge *)
(* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
let ty =
- try Retyping.get_type_of ~lax:true evenv evd body
+ try Retyping.get_type_of ~lax:true evenv evd (EConstr.of_constr body)
with Retyping.RetypeError _ -> error "Ill-typed evar instance"
in
match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with
@@ -1365,7 +1365,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
| (id,p)::_::_ ->
if choose then (mkVar id, p) else raise (NotUniqueInType sols)
in
- let ty = lazy (Retyping.get_type_of env !evdref t) in
+ let ty = lazy (Retyping.get_type_of env !evdref (EConstr.of_constr t)) in
let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in
evdref := evd;
c
@@ -1428,7 +1428,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
if not !progress then
raise (NotEnoughInformationEvarEvar t);
(* Make the virtual left evar real *)
- let ty = get_type_of env' evd t in
+ let ty = get_type_of env' evd (EConstr.of_constr t) in
let (evd,evar'',ev'') =
materialize_evar (evar_define conv_algo ~choose) env' evd k ev ty in
(* materialize_evar may instantiate ev' by another evar; adjust it *)
@@ -1462,7 +1462,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
| _ -> None
with
| Some l ->
- let ty = get_type_of env' !evdref t in
+ let ty = get_type_of env' !evdref (EConstr.of_constr t) in
let candidates =
try
let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 70e94b4dc..ac082d1bf 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -76,4 +76,4 @@ val remove_instance_local_defs :
evar_map -> existential_key -> constr array -> constr list
val get_type_of_refresh :
- ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types
+ ?polyprop:bool -> ?lax:bool -> env -> evar_map -> EConstr.constr -> evar_map * types
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a3cca2ad8..a9184777d 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -606,7 +606,7 @@ let rec instantiate_universes env evdref scl is = function
let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
match mip.mind_arity with
- | RegularArity s -> sigma, subst_instance_constr u s.mind_user_arity
+ | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity)
| TemplateArity ar ->
let _,scl = splay_arity env sigma conclty in
let ctx = List.rev mip.mind_arity_ctxt in
@@ -614,7 +614,7 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
let ctx =
instantiate_universes
env evdref scl ar.template_level (ctx,ar.template_param_levels) in
- !evdref, mkArity (List.rev ctx,scl)
+ !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl))
let type_of_projection_knowing_arg env sigma p c ty =
let c = EConstr.Unsafe.to_constr c in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 1cfdef6e5..e375a2c6b 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -195,7 +195,7 @@ i*)
(********************)
val type_of_inductive_knowing_conclusion :
- env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * types
+ env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * EConstr.types
(********************)
val control_only_guard : env -> types -> unit
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 9dcb5d2a5..938b6b18e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -153,7 +153,7 @@ let pattern_of_constr env sigma t =
| Ind (sp,u) -> PRef (canonical_gr (IndRef sp))
| Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
| Proj (p, c) ->
- pattern_of_constr env (Retyping.expand_projection env sigma p c [])
+ pattern_of_constr env (Retyping.expand_projection env sigma p (EConstr.of_constr c) [])
| Evar (evk,ctxt as ev) ->
(match snd (Evd.evar_source evk sigma) with
| Evar_kinds.MatchingVar (b,id) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2f42ad395..3c48c42df 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -409,7 +409,7 @@ let invert_ltac_bound_name lvar env id0 id =
str " which is not bound in current context.")
let protected_get_type_of env sigma c =
- try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
+ try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma (EConstr.of_constr c)
with Retyping.RetypeError _ ->
user_err
(str "Cannot reinterpret " ++ quote (print_constr c) ++
@@ -563,7 +563,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let hyps = evar_filtered_context (Evd.find !evdref evk) in
let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in
let c = mkEvar (evk, args) in
- let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
+ let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref (EConstr.of_constr c)) in
inh_conv_coerce_to_tycon loc env evdref j tycon
| GPatVar (loc,(someta,n)) ->
@@ -757,7 +757,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let sigma = !evdref in
let c = mkApp (f,Array.map (whd_evar sigma) args) in
let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in
- let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in
+ let t = Retyping.get_type_of env.ExtraEnv.env !evdref (EConstr.of_constr c) in
make_judge c (* use this for keeping evars: resj.uj_val *) t
else resj
| _ -> resj
@@ -1067,7 +1067,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
| Some v ->
let s =
let sigma = !evdref in
- let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
+ let t = Retyping.get_type_of env.ExtraEnv.env sigma (EConstr.of_constr v) in
match kind_of_term (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t)) with
| Sort s -> s
| Evar ev when is_Type (existential_type sigma ev) ->
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 353bdbb89..2efb02417 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -49,12 +49,21 @@ let anomaly_on_error f x =
try f x
with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e)
+let local_assum (na, t) =
+ let inj = EConstr.Unsafe.to_constr in
+ LocalAssum (na, inj t)
+
+let local_def (na, b, t) =
+ let inj = EConstr.Unsafe.to_constr in
+ LocalDef (na, inj b, inj t)
+
let get_type_from_constraints env sigma t =
- if isEvar (fst (decompose_app t)) then
+ let open EConstr in
+ if isEvar sigma (EConstr.of_constr (fst (decompose_app_vect sigma t))) then
match
List.map_filter (fun (pbty,env,t1,t2) ->
- if is_fconv Reduction.CONV env sigma (EConstr.of_constr t) (EConstr.of_constr t1) then Some t2
- else if is_fconv Reduction.CONV env sigma (EConstr.of_constr t) (EConstr.of_constr t2) then Some t1
+ if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t1) then Some t2
+ else if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t2) then Some t1
else None)
(snd (Evd.extract_all_conv_pbs sigma))
with
@@ -65,87 +74,89 @@ let get_type_from_constraints env sigma t =
let rec subst_type env sigma typ = function
| [] -> typ
| h::rest ->
- match kind_of_term (whd_all env sigma (EConstr.of_constr typ)) with
- | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest
+ let open EConstr in
+ match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma typ)) with
+ | Prod (na,c1,c2) -> subst_type env sigma (Vars.subst1 h c2) rest
| _ -> retype_error NonFunctionalConstruction
(* If ft is the type of f which itself is applied to args, *)
(* [sort_of_atomic_type] computes ft[args] which has to be a sort *)
let sort_of_atomic_type env sigma ft args =
+ let open EConstr in
let rec concl_of_arity env n ar args =
- match kind_of_term (whd_all env sigma (EConstr.of_constr ar)), args with
- | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l
+ match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma ar)), args with
+ | Prod (na, t, b), h::l -> concl_of_arity (push_rel (local_def (na, Vars.lift n h, t)) env) (n + 1) b l
| Sort s, [] -> s
| _ -> retype_error NotASort
in concl_of_arity env 0 ft (Array.to_list args)
let type_of_var env id =
- try NamedDecl.get_type (lookup_named id env)
+ try EConstr.of_constr (NamedDecl.get_type (lookup_named id env))
with Not_found -> retype_error (BadVariable id)
let decomp_sort env sigma t =
- match kind_of_term (whd_all env sigma t) with
+ match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
| Sort s -> s
| _ -> retype_error NotASort
let retype ?(polyprop=true) sigma =
+ let open EConstr in
let rec type_of env cstr =
- match kind_of_term cstr with
+ match EConstr.kind sigma cstr with
| Meta n ->
- (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus)
+ EConstr.of_constr (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus)
with Not_found -> retype_error (BadMeta n))
| Rel n ->
- let ty = RelDecl.get_type (lookup_rel n env) in
- lift n ty
+ let ty = EConstr.of_constr (RelDecl.get_type (lookup_rel n env)) in
+ Vars.lift n ty
| Var id -> type_of_var env id
- | Const cst -> rename_type_of_constant env cst
- | Evar ev -> Evd.existential_type sigma ev
- | Ind ind -> rename_type_of_inductive env ind
- | Construct cstr -> rename_type_of_constructor env cstr
+ | Const cst -> EConstr.of_constr (rename_type_of_constant env cst)
+ | Evar (evk, args) -> EConstr.of_constr (Evd.existential_type sigma (evk, Array.map EConstr.Unsafe.to_constr args))
+ | Ind ind -> EConstr.of_constr (rename_type_of_inductive env ind)
+ | Construct cstr -> EConstr.of_constr (rename_type_of_constructor env cstr)
| Case (_,p,c,lf) ->
let Inductiveops.IndType(indf,realargs) =
let t = type_of env c in
- try Inductiveops.find_rectype env sigma (EConstr.of_constr t)
+ try Inductiveops.find_rectype env sigma t
with Not_found ->
try
- let t = get_type_from_constraints env sigma t in
- Inductiveops.find_rectype env sigma (EConstr.of_constr t)
+ let t = EConstr.of_constr (get_type_from_constraints env sigma t) in
+ Inductiveops.find_rectype env sigma t
with Not_found -> retype_error BadRecursiveType
in
let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
- let t = betazetaevar_applist sigma n (EConstr.of_constr p) (List.map EConstr.of_constr realargs) in
- (match kind_of_term (whd_all env sigma (EConstr.of_constr (type_of env t))) with
- | Prod _ -> whd_beta sigma (EConstr.of_constr (applist (t, [c])))
+ let t = EConstr.of_constr (betazetaevar_applist sigma n p (List.map EConstr.of_constr realargs)) in
+ (match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma (type_of env t))) with
+ | Prod _ -> EConstr.of_constr (whd_beta sigma (applist (t, [c])))
| _ -> t)
| Lambda (name,c1,c2) ->
- mkProd (name, c1, type_of (push_rel (LocalAssum (name,c1)) env) c2)
+ mkProd (name, c1, type_of (push_rel (local_assum (name,c1)) env) c2)
| LetIn (name,b,c1,c2) ->
- subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2)
+ Vars.subst1 b (type_of (push_rel (local_def (name,b,c1)) env) c2)
| Fix ((_,i),(_,tys,_)) -> tys.(i)
| CoFix (i,(_,tys,_)) -> tys.(i)
- | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) ->
- let f = whd_evar sigma f in
+ | App(f,args) when is_template_polymorphic env sigma f ->
let t = type_of_global_reference_knowing_parameters env f args in
- strip_outer_cast sigma (EConstr.of_constr (subst_type env sigma t (Array.to_list args)))
+ EConstr.of_constr (strip_outer_cast sigma (subst_type env sigma t (Array.to_list args)))
| App(f,args) ->
- strip_outer_cast sigma
- (EConstr.of_constr (subst_type env sigma (type_of env f) (Array.to_list args)))
+ EConstr.of_constr (strip_outer_cast sigma
+ (subst_type env sigma (type_of env f) (Array.to_list args)))
| Proj (p,c) ->
let ty = type_of env c in
- (try
- Inductiveops.type_of_projection_knowing_arg env sigma p (EConstr.of_constr c) (EConstr.of_constr ty)
+ EConstr.of_constr (try
+ Inductiveops.type_of_projection_knowing_arg env sigma p c ty
with Invalid_argument _ -> retype_error BadRecursiveType)
| Cast (c,_, t) -> t
| Sort _ | Prod _ -> mkSort (sort_of env cstr)
and sort_of env t =
- match kind_of_term t with
- | Cast (c,_, s) when isSort s -> destSort s
+ match EConstr.kind sigma t with
+ | Cast (c,_, s) when isSort sigma s -> destSort sigma s
| Sort (Prop c) -> type1_sort
| Sort (Type u) -> Type (Univ.super u)
| Prod (name,t,c2) ->
- (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with
+ (match (sort_of env t, sort_of (push_rel (local_assum (name,t)) env) c2) with
| _, (Prop Null as s) -> s
| Prop _, (Prop Pos as s) -> s
| Type _, (Prop Pos as s) when is_impredicative_set env -> s
@@ -153,47 +164,45 @@ let retype ?(polyprop=true) sigma =
| Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
| Prop Null, (Type _ as s) -> s
| Type u1, Type u2 -> Type (Univ.sup u1 u2))
- | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) ->
- let f = whd_evar sigma f in
+ | App(f,args) when is_template_polymorphic env sigma f ->
let t = type_of_global_reference_knowing_parameters env f args in
sort_of_atomic_type env sigma t args
| App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
| Lambda _ | Fix _ | Construct _ -> retype_error NotAType
- | _ -> decomp_sort env sigma (EConstr.of_constr (type_of env t))
+ | _ -> decomp_sort env sigma (type_of env t)
and sort_family_of env t =
- match kind_of_term t with
- | Cast (c,_, s) when isSort s -> family_of_sort (destSort s)
+ match EConstr.kind sigma t with
+ | Cast (c,_, s) when isSort sigma s -> family_of_sort (destSort sigma s)
| Sort (Prop c) -> InType
| Sort (Type u) -> InType
| Prod (name,t,c2) ->
- let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
+ let s2 = sort_family_of (push_rel (local_assum (name,t)) env) c2 in
if not (is_impredicative_set env) &&
s2 == InSet && sort_family_of env t == InType then InType else s2
- | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) ->
- let f = whd_evar sigma f in
+ | App(f,args) when is_template_polymorphic env sigma f ->
let t = type_of_global_reference_knowing_parameters env f args in
family_of_sort (sort_of_atomic_type env sigma t args)
| App(f,args) ->
family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
| Lambda _ | Fix _ | Construct _ -> retype_error NotAType
| _ ->
- family_of_sort (decomp_sort env sigma (EConstr.of_constr (type_of env t)))
+ family_of_sort (decomp_sort env sigma (type_of env t))
and type_of_global_reference_knowing_parameters env c args =
let argtyps =
- Array.map (fun c -> lazy (nf_evar sigma (type_of env c))) args in
- match kind_of_term c with
+ Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in
+ match EConstr.kind sigma c with
| Ind ind ->
let mip = lookup_mind_specif env (fst ind) in
- (try Inductive.type_of_inductive_knowing_parameters
+ EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters
~polyprop env (mip,snd ind) argtyps
with Reduction.NotArity -> retype_error NotAnArity)
| Const cst ->
- (try Typeops.type_of_constant_knowing_parameters_in env cst argtyps
+ EConstr.of_constr (try Typeops.type_of_constant_knowing_parameters_in env cst argtyps
with Reduction.NotArity -> retype_error NotAnArity)
| Var id -> type_of_var env id
- | Construct cstr -> type_of_constructor env cstr
+ | Construct cstr -> EConstr.of_constr (type_of_constructor env cstr)
| _ -> assert false
in type_of, sort_of, sort_family_of,
@@ -204,19 +213,19 @@ let get_sort_of ?(polyprop=true) env sigma t =
let get_sort_family_of ?(polyprop=true) env sigma c =
let _,_,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) c
let type_of_global_reference_knowing_parameters env sigma c args =
- let _,_,_,f = retype sigma in anomaly_on_error (f env c) args
+ let _,_,_,f = retype sigma in EConstr.Unsafe.to_constr (anomaly_on_error (f env c) args)
let type_of_global_reference_knowing_conclusion env sigma c conclty =
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Ind (ind,u) ->
let spec = Inductive.lookup_mind_specif env ind in
- type_of_inductive_knowing_conclusion env sigma (spec,u) (EConstr.of_constr conclty)
+ type_of_inductive_knowing_conclusion env sigma (spec,u) conclty
| Const cst ->
let t = constant_type_in env cst in
(* TODO *)
- sigma, Typeops.type_of_constant_type_knowing_parameters env t [||]
+ sigma, EConstr.of_constr (Typeops.type_of_constant_type_knowing_parameters env t [||])
| Var id -> sigma, type_of_var env id
- | Construct cstr -> sigma, type_of_constructor env cstr
+ | Construct cstr -> sigma, EConstr.of_constr (type_of_constructor env cstr)
| _ -> assert false
(* Profiling *)
@@ -232,10 +241,10 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
let get_type_of ?(polyprop=true) ?(lax=false) env sigma c =
let f,_,_,_ = retype ~polyprop sigma in
- if lax then f env c else anomaly_on_error (f env) c
+ if lax then EConstr.Unsafe.to_constr (f env c) else EConstr.Unsafe.to_constr (anomaly_on_error (f env) c)
(* Makes an unsafe judgment from a constr *)
-let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c }
+let get_judgment_of env evc c = { uj_val = EConstr.Unsafe.to_constr c; uj_type = get_type_of env evc c }
(* Returns sorts of a context *)
let sorts_of_context env evc ctxt =
@@ -243,15 +252,16 @@ let sorts_of_context env evc ctxt =
| [] -> env,[]
| d :: ctxt ->
let env,sorts = aux ctxt in
- let s = get_sort_of env evc (RelDecl.get_type d) in
+ let s = get_sort_of env evc (EConstr.of_constr (RelDecl.get_type d)) in
(push_rel d env,s::sorts) in
snd (aux ctxt)
let expand_projection env sigma pr c args =
+ let inj = EConstr.Unsafe.to_constr in
let ty = get_type_of ~lax:true env sigma c in
let (i,u), ind_args =
try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty)
with Not_found -> retype_error BadRecursiveType
in
mkApp (mkConstU (Projection.constant pr,u),
- Array.of_list (ind_args @ (c :: args)))
+ Array.of_list (ind_args @ (inj c :: List.map inj args)))
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 8ca40f829..08f750287 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -26,25 +26,25 @@ type retype_error
exception RetypeError of retype_error
val get_type_of :
- ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types
+ ?polyprop:bool -> ?lax:bool -> env -> evar_map -> EConstr.constr -> types
val get_sort_of :
- ?polyprop:bool -> env -> evar_map -> types -> sorts
+ ?polyprop:bool -> env -> evar_map -> EConstr.types -> sorts
val get_sort_family_of :
- ?polyprop:bool -> env -> evar_map -> types -> sorts_family
+ ?polyprop:bool -> env -> evar_map -> EConstr.types -> sorts_family
(** Makes an unsafe judgment from a constr *)
-val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
+val get_judgment_of : env -> evar_map -> EConstr.constr -> unsafe_judgment
-val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
- constr array -> types
+val type_of_global_reference_knowing_parameters : env -> evar_map -> EConstr.constr ->
+ EConstr.constr array -> types
val type_of_global_reference_knowing_conclusion :
- env -> evar_map -> constr -> types -> evar_map * types
+ env -> evar_map -> EConstr.constr -> EConstr.types -> evar_map * EConstr.types
val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list
-val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
+val expand_projection : env -> evar_map -> Names.projection -> EConstr.constr -> EConstr.constr list -> constr
val print_retype_error : retype_error -> Pp.std_ppcmds
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 357a80f44..ac2a3bc49 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -974,7 +974,7 @@ let matches_head env sigma c t =
let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
match kind_of_term c with
| Proj (p, r) -> (* Treat specially for partial applications *)
- let t = Retyping.expand_projection env sigma p r [] in
+ let t = Retyping.expand_projection env sigma p (EConstr.of_constr r) [] in
let hdf, al = destApp t in
let a = al.(Array.length al - 1) in
let app = (mkApp (hdf, Array.sub al 0 (Array.length al - 1))) in
@@ -1150,7 +1150,7 @@ let compute = cbv_betadeltaiota
* the specified occurrences. *)
let abstract_scheme env (locc,a) (c, sigma) =
- let ta = Retyping.get_type_of env sigma a in
+ let ta = Retyping.get_type_of env sigma (EConstr.of_constr a) in
let na = named_hd env ta Anonymous in
if occur_meta sigma (EConstr.of_constr ta) then error "Cannot find a type for the generalisation.";
if occur_meta sigma (EConstr.of_constr a) then
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 50dd66ea0..8c03329e2 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -300,7 +300,7 @@ let build_subclasses ~check env sigma glob pri =
| Some (Forward, pri') ->
let proj = Option.get proj in
let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
- if check && check_instance env sigma body then None
+ if check && check_instance env sigma (EConstr.of_constr body) then None
else
let pri =
match pri, pri' with
@@ -312,7 +312,7 @@ let build_subclasses ~check env sigma glob pri =
in
let declare_proj hints (cref, pri, body) =
let path' = cref :: path in
- let ty = Retyping.get_type_of env sigma body in
+ let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in
let rest = aux pri body ty path' in
hints @ (path', pri, body) :: rest
in List.fold_left declare_proj [] projs
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e3d1c1741..acfe05f24 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -138,7 +138,7 @@ let check_type_fixpoint loc env evdref lna lar vdefj =
(* FIXME: might depend on the level of actual parameters!*)
let check_allowed_sort env sigma ind c p =
- let pj = Retyping.get_judgment_of env sigma p in
+ let pj = Retyping.get_judgment_of env sigma (EConstr.of_constr p) in
let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in
let specif = Global.lookup_inductive (fst ind) in
let sorts = elim_sorts specif in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ede2606da..848a2f4a8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -684,7 +684,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
if opt.with_types && flags.check_applied_meta_types then
(try
let tyM = Typing.meta_type sigma k in
- let tyN = get_type_of curenv ~lax:true sigma cN in
+ let tyN = get_type_of curenv ~lax:true sigma (EConstr.of_constr cN) in
check_compatibility curenv CUMUL flags substn tyN tyM
with RetypeError _ ->
(* Renounce, maybe metas/evars prevents typing *) sigma)
@@ -703,7 +703,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
let sigma =
if opt.with_types && flags.check_applied_meta_types then
(try
- let tyM = get_type_of curenv ~lax:true sigma cM in
+ let tyM = get_type_of curenv ~lax:true sigma (EConstr.of_constr cM) in
let tyN = Typing.meta_type sigma k in
check_compatibility curenv CUMUL flags substn tyM tyN
with RetypeError _ ->
@@ -863,7 +863,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
let expand_proj c c' l =
match kind_of_term c with
| Proj (p, t) when not (Projection.unfolded p) && needs_expansion p c' ->
- (try destApp (Retyping.expand_projection curenv sigma p t (Array.to_list l))
+ (try destApp (Retyping.expand_projection curenv sigma p (EConstr.of_constr t) (Array.map_to_list EConstr.of_constr l))
with RetypeError _ -> (** Unification can be called on ill-typed terms, due
to FO and eta in particular, fail gracefully in that case *)
(c, l))
@@ -888,8 +888,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
and unify_same_proj (curenv, nb as curenvnb) cv_pb opt substn c1 c2 =
let substn = unirec_rec curenvnb CONV opt substn c1 c2 in
try (* Force unification of the types to fill in parameters *)
- let ty1 = get_type_of curenv ~lax:true sigma c1 in
- let ty2 = get_type_of curenv ~lax:true sigma c2 in
+ let ty1 = get_type_of curenv ~lax:true sigma (EConstr.of_constr c1) in
+ let ty2 = get_type_of curenv ~lax:true sigma (EConstr.of_constr c2) in
unify_0_with_initial_metas substn true curenv cv_pb
{ flags with modulo_conv_on_closed_terms = Some full_transparent_state;
modulo_delta = full_transparent_state;
@@ -953,8 +953,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
let sigma =
if opt.with_types then
try (* Ensure we call conversion on terms of the same type *)
- let tyM = get_type_of curenv ~lax:true sigma m1 in
- let tyN = get_type_of curenv ~lax:true sigma n1 in
+ let tyM = get_type_of curenv ~lax:true sigma (EConstr.of_constr m1) in
+ let tyN = get_type_of curenv ~lax:true sigma (EConstr.of_constr n1) in
check_compatibility curenv CUMUL flags substn tyM tyN
with RetypeError _ ->
(* Renounce, maybe metas/evars prevents typing *) sigma
@@ -1240,13 +1240,13 @@ let w_coerce_to_type env evd c cty mvty =
try_to_coerce env evd c cty tycon
let w_coerce env evd mv c =
- let cty = get_type_of env evd c in
+ let cty = get_type_of env evd (EConstr.of_constr c) in
let mvty = Typing.meta_type evd mv in
w_coerce_to_type env evd c cty mvty
let unify_to_type env sigma flags c status u =
let sigma, c = refresh_universes (Some false) env sigma c in
- let t = get_type_of env sigma (nf_meta sigma c) in
+ let t = get_type_of env sigma (EConstr.of_constr (nf_meta sigma c)) in
let t = nf_betaiota sigma (EConstr.of_constr (nf_meta sigma t)) in
unify_0 env sigma CUMUL flags t u
@@ -1379,7 +1379,7 @@ let w_merge env with_types flags (evd,metas,evars) =
let evd' = Sigma.to_evar_map evd' in
let (evd'',mc,ec) =
unify_0 sp_env evd' CUMUL flags
- (get_type_of sp_env evd' c) ev.evar_concl in
+ (get_type_of sp_env evd' (EConstr.of_constr c)) ev.evar_concl in
let evd''' = w_merge_rec evd'' mc ec [] in
if evd' == evd'''
then Evd.define sp c evd'''
@@ -1422,13 +1422,13 @@ let check_types env flags (sigma,_,_ as subst) m n =
if isEvar_or_Meta (head_app sigma m) then
unify_0_with_initial_metas subst true env CUMUL
flags
- (get_type_of env sigma n)
- (get_type_of env sigma m)
+ (get_type_of env sigma (EConstr.of_constr n))
+ (get_type_of env sigma (EConstr.of_constr m))
else if isEvar_or_Meta (head_app sigma n) then
unify_0_with_initial_metas subst true env CUMUL
flags
- (get_type_of env sigma m)
- (get_type_of env sigma n)
+ (get_type_of env sigma (EConstr.of_constr m))
+ (get_type_of env sigma (EConstr.of_constr n))
else subst
let try_resolve_typeclasses env evd flag m n =
@@ -1557,7 +1557,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
applist (t,l1), l2
else t, [] in
let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in
- let ty = Retyping.get_type_of env sigma t in
+ let ty = Retyping.get_type_of env sigma (EConstr.of_constr t) in
if not (is_correct_type ty) then raise (NotUnifiable None);
Some(sigma, t, l2)
with
@@ -1590,7 +1590,7 @@ let make_eq_test env evd c =
let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
let id =
- let t = match ty with Some t -> t | None -> get_type_of env sigma c in
+ let t = match ty with Some t -> t | None -> get_type_of env sigma (EConstr.of_constr c) in
let x = id_of_name_using_hdchar (Global.env()) t name in
let ids = ids_of_named_context (named_context env) in
if name == Anonymous then next_ident_away_in_goal x ids else
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 03:51:14 +0000