aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evarutil.ml8
-rw-r--r--engine/evarutil.mli4
-rw-r--r--engine/termops.ml4
-rw-r--r--engine/termops.mli4
-rw-r--r--pretyping/cases.ml14
-rw-r--r--pretyping/inductiveops.ml14
-rw-r--r--pretyping/inductiveops.mli12
-rw-r--r--pretyping/pretyping.ml1
-rw-r--r--pretyping/retyping.ml2
-rw-r--r--tactics/inv.ml1
-rw-r--r--tactics/leminv.ml50
-rw-r--r--tactics/tactics.ml9
-rw-r--r--toplevel/command.ml4
13 files changed, 70 insertions, 57 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index c2ad3c462..35fe9cf66 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -68,6 +68,9 @@ let rec flush_and_check_evars sigma c =
| Some c -> flush_and_check_evars sigma c)
| _ -> map_constr (flush_and_check_evars sigma) c
+let flush_and_check_evars sigma c =
+ flush_and_check_evars sigma (EConstr.Unsafe.to_constr c)
+
(* let nf_evar_key = Profile.declare_profile "nf_evar" *)
(* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *)
@@ -474,12 +477,13 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami
(* This assumes an evar with identity instance and generalizes it over only
the De Bruijn part of the context *)
let generalize_evar_over_rels sigma (ev,args) =
+ let open EConstr in
let evi = Evd.find sigma ev in
let sign = named_context_of_val evi.evar_hyps in
List.fold_left2
(fun (c,inst as x) a d ->
- if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
- (evi.evar_concl,[]) (Array.to_list args) sign
+ if isRel sigma a then (mkNamedProd_or_LetIn d c,a::inst) else x)
+ (EConstr.of_constr evi.evar_concl,[]) (Array.to_list args) sign
(************************************)
(* Removing a dependency in an evar *)
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 82346b24e..ad3851ea3 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -170,7 +170,7 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
(** Replacing all evars, possibly raising [Uninstantiated_evar] *)
exception Uninstantiated_evar of existential_key
-val flush_and_check_evars : evar_map -> constr -> constr
+val flush_and_check_evars : evar_map -> EConstr.constr -> constr
(** {6 Term manipulation up to instantiation} *)
@@ -220,7 +220,7 @@ val push_rel_decl_to_named_context :
val push_rel_context_to_named_context : Environ.env -> EConstr.types ->
named_context_val * EConstr.types * EConstr.constr list * csubst * (identifier*EConstr.constr) list
-val generalize_evar_over_rels : evar_map -> existential -> types * constr list
+val generalize_evar_over_rels : evar_map -> EConstr.existential -> EConstr.types * EConstr.constr list
(** Evar combinators *)
diff --git a/engine/termops.ml b/engine/termops.ml
index 4ab9f0733..ef7cdc38b 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -233,9 +233,9 @@ let it_named_context_quantifier f ~init =
let it_mkProd_or_LetIn init = it_named_context_quantifier mkProd_or_LetIn ~init
let it_mkProd_wo_LetIn init = it_named_context_quantifier mkProd_wo_LetIn ~init
let it_mkLambda_or_LetIn init = it_named_context_quantifier mkLambda_or_LetIn ~init
-let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_LetIn ~init
+let it_mkNamedProd_or_LetIn init = it_named_context_quantifier EConstr.mkNamedProd_or_LetIn ~init
let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init
-let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
+let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier EConstr.mkNamedLambda_or_LetIn ~init
let it_mkLambda_or_LetIn_from_no_LetIn c decls =
let open RelDecl in
diff --git a/engine/termops.mli b/engine/termops.mli
index 1c14e6c89..72c0cedda 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -51,9 +51,9 @@ val it_mkLambda : EConstr.constr -> (Name.t * EConstr.types) list -> EConstr.con
val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
val it_mkProd_wo_LetIn : EConstr.types -> Context.Rel.t -> EConstr.types
val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
-val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types
+val it_mkNamedProd_or_LetIn : EConstr.types -> Context.Named.t -> EConstr.types
val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types
-val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr
+val it_mkNamedLambda_or_LetIn : EConstr.constr -> Context.Named.t -> EConstr.constr
(* Ad hoc version reinserting letin, assuming the body is defined in
the context where the letins are expanded *)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 360199fec..119e92c82 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -326,7 +326,7 @@ let inh_coerce_to_ind evdref env loc ty tyi =
let binding_vars_of_inductive sigma = function
| NotInd _ -> []
- | IsInd (_,IndType(_,realargs),_) -> List.filter (isRel sigma) (List.map EConstr.of_constr realargs)
+ | IsInd (_,IndType(_,realargs),_) -> List.filter (isRel sigma) realargs
let extract_inductive_data env sigma decl =
match decl with
@@ -422,7 +422,7 @@ let type_of_tomatch = function
| NotInd (_,t) -> t
let map_tomatch_type f = function
- | IsInd (t,ind,names) -> IsInd (f t,map_inductive_type (fun c -> EConstr.Unsafe.to_constr (f (EConstr.of_constr c))) ind,names)
+ | IsInd (t,ind,names) -> IsInd (f t,map_inductive_type f ind,names)
| NotInd (c,t) -> NotInd (Option.map f c, f t)
let liftn_tomatch_type n depth = map_tomatch_type (Vars.liftn n depth)
@@ -873,7 +873,7 @@ let specialize_predicate_var (cur,typ,dep) tms ccl =
let l =
match typ with
| IsInd (_, IndType (_, _), []) -> []
- | IsInd (_, IndType (_, realargs), names) -> List.map EConstr.of_constr realargs
+ | IsInd (_, IndType (_, realargs), names) -> realargs
| NotInd _ -> [] in
subst_predicate (l,c) ccl tms
@@ -922,7 +922,7 @@ let rec extract_predicate ccl = function
subst1 cur pred
end
| Pushed (_,((cur,IsInd (_,IndType(_,realargs),_)),_,na))::tms ->
- let realargs = List.rev_map EConstr.of_constr realargs in
+ let realargs = List.rev realargs in
let k, nrealargs = match na with
| Anonymous -> 0, realargs
| Name _ -> 1, (cur :: realargs)
@@ -1064,7 +1064,6 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
snd (List.fold_left (expand_arg tms) (1,ccl''') newtomatchs)
let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
- let realargs = List.map EConstr.of_constr realargs in
let pred = abstract_predicate env !evdref indf current realargs dep tms p in
(pred, EConstr.of_constr (whd_betaiota !evdref
(applist (pred, realargs@[current]))))
@@ -1384,7 +1383,6 @@ and match_current pb (initial,tomatch) =
if (not no_cstr || not (List.is_empty pb.mat)) && onlydflt then
compile_all_variables initial tomatch pb
else
- let realargs = List.map EConstr.of_constr realargs in
(* We generalize over terms depending on current term to match *)
let pb,deps = generalize_problem (names,dep) pb deps in
@@ -1749,7 +1747,6 @@ let build_inversion_problem loc env sigma tms t =
match tms with
| [] -> [], acc_sign, acc
| (t, IsInd (_,IndType(indf,realargs),_)) :: tms ->
- let realargs = List.map EConstr.of_constr realargs in
let patl,acc = List.fold_map' reveal_pattern realargs acc in
let pat,acc = make_patvar t acc in
let indf' = lift_inductive_family n indf in
@@ -1919,7 +1916,6 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
(match tmtype with
NotInd _ -> (subst, len - signlen)
| IsInd (_, IndType(indf,realargs),_) ->
- let realargs = List.map EConstr.of_constr realargs in
let subst, len =
List.fold_left
(fun (subst, len) arg ->
@@ -2119,7 +2115,6 @@ let constr_of_pat env evdref arsign pat avoid =
let apptype = Retyping.get_type_of env ( !evdref) app in
let apptype = EConstr.of_constr apptype in
let IndType (indf, realargs) = find_rectype env (!evdref) apptype in
- let realargs = List.map EConstr.of_constr realargs in
match alias with
Anonymous ->
pat', sign, app, apptype, realargs, n, avoid
@@ -2364,7 +2359,6 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
*)
match ty with
| IsInd (ty, IndType (indf, args), _) when List.length args > 0 ->
- let args = List.map EConstr.of_constr args in
(* Build the arity signature following the names in matched terms
as much as possible *)
let argsign = List.tl arsign in (* arguments in inverse application order *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 98b267cfd..cb8b25323 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -58,21 +58,23 @@ let lift_inductive_family n = liftn_inductive_family n 1
let substnl_ind_family l n = map_ind_family (substnl l n)
-type inductive_type = IndType of inductive_family * constr list
+type inductive_type = IndType of inductive_family * EConstr.constr list
let make_ind_type (indf, realargs) = IndType (indf,realargs)
let dest_ind_type (IndType (indf,realargs)) = (indf,realargs)
let map_inductive_type f (IndType (indf, realargs)) =
- IndType (map_ind_family f indf, List.map f realargs)
+ let f' c = EConstr.Unsafe.to_constr (f (EConstr.of_constr c)) in
+ IndType (map_ind_family f' indf, List.map f realargs)
-let liftn_inductive_type n d = map_inductive_type (liftn n d)
+let liftn_inductive_type n d = map_inductive_type (EConstr.Vars.liftn n d)
let lift_inductive_type n = liftn_inductive_type n 1
-let substnl_ind_type l n = map_inductive_type (substnl l n)
+let substnl_ind_type l n = map_inductive_type (EConstr.Vars.substnl l n)
let mkAppliedInd (IndType ((ind,params), realargs)) =
- applist (mkIndU ind,params@realargs)
+ let open EConstr in
+ applist (mkIndU ind, (List.map EConstr.of_constr params)@realargs)
(* Does not consider imbricated or mutually recursive types *)
let mis_is_recursive_subset listind rarg =
@@ -471,7 +473,7 @@ let find_rectype env sigma c =
if mib.mind_nparams > List.length l then raise Not_found;
let l = List.map EConstr.Unsafe.to_constr l in
let (par,rargs) = List.chop mib.mind_nparams l in
- IndType((indu, par),rargs)
+ IndType((indu, par),List.map EConstr.of_constr rargs)
| _ -> raise Not_found
let find_inductive env sigma c =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7af9731f9..1614e1817 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -37,15 +37,15 @@ val substnl_ind_family :
constr list -> int -> inductive_family -> inductive_family
(** An inductive type with its parameters and real arguments *)
-type inductive_type = IndType of inductive_family * constr list
-val make_ind_type : inductive_family * constr list -> inductive_type
-val dest_ind_type : inductive_type -> inductive_family * constr list
-val map_inductive_type : (constr -> constr) -> inductive_type -> inductive_type
+type inductive_type = IndType of inductive_family * EConstr.constr list
+val make_ind_type : inductive_family * EConstr.constr list -> inductive_type
+val dest_ind_type : inductive_type -> inductive_family * EConstr.constr list
+val map_inductive_type : (EConstr.constr -> EConstr.constr) -> inductive_type -> inductive_type
val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
val lift_inductive_type : int -> inductive_type -> inductive_type
-val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type
+val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type
-val mkAppliedInd : inductive_type -> constr
+val mkAppliedInd : inductive_type -> EConstr.constr
val mis_is_recursive_subset : int list -> wf_paths -> bool
val mis_is_recursive :
inductive * mutual_inductive_body * one_inductive_body -> bool
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7586b54ba..11d50926f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -860,7 +860,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let cloc = loc_of_glob_constr c in
error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj
in
- let realargs = List.map EConstr.of_constr realargs in
let cstrs = get_constructors env.ExtraEnv.env indf in
if not (Int.equal (Array.length cstrs) 1) then
user_err ~loc (str "Destructing let is only for inductive types" ++
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 6f03fc462..88899e633 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -123,7 +123,7 @@ let retype ?(polyprop=true) sigma =
with Not_found -> retype_error BadRecursiveType
in
let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
- let t = EConstr.of_constr (betazetaevar_applist sigma n p (List.map EConstr.of_constr realargs)) in
+ let t = EConstr.of_constr (betazetaevar_applist sigma n p 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)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 37c82ff64..5c296b343 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -450,7 +450,6 @@ let raw_inversion inv_kind id status names =
CErrors.user_err msg
in
let IndType (indf,realargs) = find_rectype env sigma t in
- let realargs = List.map EConstr.of_constr realargs in
let evdref = ref sigma in
let (elim_predicate, args) =
make_inv_predicate env evdref indf realargs id status concl in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a94238418..62e78b588 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -11,8 +11,9 @@ open CErrors
open Util
open Names
open Term
-open Vars
open Termops
+open EConstr
+open Vars
open Namegen
open Evd
open Printer
@@ -31,9 +32,17 @@ open Context.Named.Declaration
module NamedDecl = Context.Named.Declaration
+let nlocal_assum (na, t) =
+ let inj = EConstr.Unsafe.to_constr in
+ NamedDecl.LocalAssum (na, inj t)
+
+let nlocal_def (na, b, t) =
+ let inj = EConstr.Unsafe.to_constr in
+ NamedDecl.LocalDef (na, inj b, inj t)
+
let no_inductive_inconstr env sigma constr =
(str "Cannot recognize an inductive predicate in " ++
- pr_lconstr_env env sigma constr ++
+ pr_lconstr_env env sigma (EConstr.Unsafe.to_constr constr) ++
str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++
spc () ++ str "or of the type of constructors" ++ spc () ++
str "is hidden by constant definitions.")
@@ -116,15 +125,15 @@ let max_prefix_sign lid sign =
| id::l -> snd (max_rec (id, sign_prefix id sign) l)
*)
let rec add_prods_sign env sigma t =
- match kind_of_term (whd_all env sigma (EConstr.of_constr t)) with
+ match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
| Prod (na,c1,b) ->
- let id = id_of_name_using_hdchar env t na in
+ let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in
let b'= subst1 (mkVar id) b in
- add_prods_sign (push_named (LocalAssum (id,c1)) env) sigma b'
+ add_prods_sign (push_named (nlocal_assum (id,c1)) env) sigma b'
| LetIn (na,c1,t1,b) ->
- let id = id_of_name_using_hdchar env t na in
+ let id = id_of_name_using_hdchar env (EConstr.Unsafe.to_constr t) na in
let b'= subst1 (mkVar id) b in
- add_prods_sign (push_named (LocalDef (id,c1,t1)) env) sigma b'
+ add_prods_sign (push_named (nlocal_def (id,c1,t1)) env) sigma b'
| _ -> (env,t)
(* [dep_option] indicates whether the inversion lemma is dependent or not.
@@ -147,6 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
let pty,goal =
if dep_option then
let pty = make_arity env true indf sort in
+ let pty = EConstr.of_constr pty in
let goal =
mkProd
(Anonymous, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
@@ -154,7 +164,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
pty,goal
else
let i = mkAppliedInd ind in
- let ivars = global_vars env sigma (EConstr.of_constr i) in
+ let ivars = global_vars env sigma i in
let revargs,ownsign =
fold_named_context
(fun env d (revargs,hyps) ->
@@ -169,7 +179,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in
(pty,goal)
in
- let npty = nf_all env sigma (EConstr.of_constr pty) in
+ let npty = nf_all env sigma pty in
let extenv = push_named (LocalAssum (p,npty)) env in
extenv, goal
@@ -183,7 +193,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
let inversion_scheme env sigma t sort dep_option inv_op =
let (env,i) = add_prods_sign env sigma t in
let ind =
- try find_rectype env sigma (EConstr.of_constr i)
+ try find_rectype env sigma i
with Not_found ->
user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i)
in
@@ -192,18 +202,20 @@ let inversion_scheme env sigma t sort dep_option inv_op =
in
assert
(List.subset
- (global_vars env sigma (EConstr.of_constr invGoal))
+ (global_vars env sigma invGoal)
(ids_of_named_context (named_context invEnv)));
(*
user_err ~hdr:"lemma_inversion"
(str"Computed inversion goal was not closed in initial signature.");
*)
+ let invGoal = EConstr.Unsafe.to_constr invGoal in
let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
let pf =
fst (Proof.run_tactic env (
tclTHEN intro (onLastHypId inv_op)) pf)
in
let pfterm = List.hd (Proof.partial_proof pf) in
+ let pfterm = EConstr.of_constr pfterm in
let global_named_context = Global.named_context_val () in
let ownSign = ref begin
fold_named_context
@@ -216,18 +228,19 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let { sigma=sigma } = Proof.V82.subgoals pf in
let sigma = Evd.nf_constraints sigma in
let rec fill_holes c =
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Evar (e,args) ->
let h = next_ident_away (Id.of_string "H") !avoid in
let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
avoid := h::!avoid;
- ownSign := Context.Named.add (LocalAssum (h,ty)) !ownSign;
+ ownSign := Context.Named.add (nlocal_assum (h,ty)) !ownSign;
applist (mkVar h, inst)
- | _ -> Constr.map fill_holes c
+ | _ -> EConstr.map sigma fill_holes c
in
let c = fill_holes pfterm in
(* warning: side-effect on ownSign *)
let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
+ let invProof = EConstr.Unsafe.to_constr invProof in
let p = Evarutil.nf_evars_universes sigma invProof in
p, Evd.universe_context sigma
@@ -245,6 +258,7 @@ let add_inversion_lemma_exn na com comsort bool tac =
let env = Global.env () in
let evd = ref (Evd.from_env env) in
let c = Constrintern.interp_type_evars env evd com in
+ let c = EConstr.of_constr c in
let sigma, sort = Pretyping.interp_sort !evd comsort in
try
add_inversion_lemma na env sigma c sort bool tac
@@ -258,14 +272,16 @@ let add_inversion_lemma_exn na com comsort bool tac =
let lemInv id c gls =
try
- let clause = mk_clenv_type_of gls (EConstr.of_constr c) in
+ let clause = mk_clenv_type_of gls c in
let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
with
| NoSuchBinding ->
+ let c = EConstr.Unsafe.to_constr c in
user_err
(hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
| UserError (a,b) ->
+ let c = EConstr.Unsafe.to_constr c in
user_err ~hdr:"LemInv"
(str "Cannot refine current goal with the lemma " ++
pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
@@ -291,5 +307,5 @@ let lemInvIn id c ids =
let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
let lemInv_clause id c = function
- | [] -> lemInv_gen id (EConstr.Unsafe.to_constr c)
- | l -> lemInvIn_gen id (EConstr.Unsafe.to_constr c) l
+ | [] -> lemInv_gen id c
+ | l -> lemInvIn_gen id c l
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bae1ad48c..59ffd8b62 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2896,8 +2896,7 @@ let old_generalize_dep ?(with_let=false) c gl =
-> id::tothin
| _ -> tothin
in
- let cl' = it_mkNamedProd_or_LetIn (Tacmach.pf_concl gl) to_quantify in
- let cl' = EConstr.of_constr cl' in
+ let cl' = it_mkNamedProd_or_LetIn (EConstr.of_constr (Tacmach.pf_concl gl)) to_quantify in
let body =
if with_let then
match EConstr.kind sigma c with
@@ -4256,11 +4255,11 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
let env = Proofview.Goal.env gl in
let sigma = Sigma.to_evar_map sigma in
let concl = Tacmach.New.pf_nf_concl gl in
+ let concl = EConstr.of_constr concl in
let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env sigma in
- let dep_in_concl = Option.cata (fun id -> occur_var env sigma id (EConstr.of_constr concl)) false hyp0 in
+ let dep_in_concl = Option.cata (fun id -> occur_var env sigma id concl) false hyp0 in
let dep = dep_in_hyps || dep_in_concl in
let tmpcl = it_mkNamedProd_or_LetIn concl deps in
- let tmpcl = EConstr.of_constr tmpcl in
let s = Retyping.get_sort_family_of env sigma tmpcl in
let deps_cstr =
List.fold_left
@@ -5008,7 +5007,7 @@ let abstract_subproof id gk tac =
else (Context.Named.add d s1,s2))
global_sign (Context.Named.empty, empty_named_context_val) in
let id = next_global_ident_away id (pf_ids_of_hyps gl) in
- let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in
+ let concl = it_mkNamedProd_or_LetIn (EConstr.of_constr (Proofview.Goal.concl gl)) sign in
let concl =
try flush_and_check_evars !evdref concl
with Uninstantiated_evar _ ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 08f3ad4a7..1b5c4f660 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1271,9 +1271,9 @@ let do_program_recursive local p fixkind fixl ntns =
let collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
let def =
- nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign)
+ nf_evar evd (EConstr.Unsafe.to_constr (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign))
and typ =
- nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
+ nf_evar evd (EConstr.Unsafe.to_constr (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign))
in
let evm = collect_evars_of_term evd def typ in
let evars, _, def, typ =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 05:55:41 +0000