aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/eConstr.ml2
-rw-r--r--engine/eConstr.mli3
-rw-r--r--ltac/rewrite.ml10
-rw-r--r--pretyping/evarconv.ml12
-rw-r--r--pretyping/miscops.ml13
-rw-r--r--pretyping/miscops.mli5
-rw-r--r--pretyping/reductionops.ml8
-rw-r--r--pretyping/reductionops.mli4
-rw-r--r--pretyping/typing.ml3
-rw-r--r--pretyping/typing.mli2
-rw-r--r--pretyping/unification.ml14
-rw-r--r--proofs/clenv.ml129
-rw-r--r--proofs/clenv.mli31
-rw-r--r--proofs/clenvtac.ml17
-rw-r--r--proofs/clenvtac.mli1
-rw-r--r--tactics/auto.ml5
-rw-r--r--tactics/autorewrite.ml6
-rw-r--r--tactics/class_tactics.ml21
-rw-r--r--tactics/eauto.ml3
-rw-r--r--tactics/equality.ml38
-rw-r--r--tactics/hints.ml12
-rw-r--r--tactics/leminv.ml4
-rw-r--r--tactics/tacticals.ml12
-rw-r--r--tactics/tactics.ml70
24 files changed, 261 insertions, 164 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 095521e25..7bd708e31 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -560,6 +560,8 @@ let substn_vars n subst c = of_constr (Vars.substn_vars n subst (to_constr c))
let subst_vars subst c = of_constr (Vars.subst_vars subst (to_constr c))
let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
+let subst_univs_level_constr subst c =
+ of_constr (Vars.subst_univs_level_constr subst (to_constr c))
(** Operations that dot NOT commute with evar-normalization *)
let noccurn sigma n term =
let rec occur_rec n c = match kind sigma c with
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 10eb064a3..e4136a612 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -171,6 +171,9 @@ val noccur_between : Evd.evar_map -> int -> int -> t -> bool
val closedn : Evd.evar_map -> int -> t -> bool
val closed0 : Evd.evar_map -> t -> bool
+
+val subst_univs_level_constr : Univ.universe_level_subst -> t -> t
+
end
(** {5 Unsafe operations} *)
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 37b9a9edb..52cf1ff35 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -507,9 +507,12 @@ let decompose_applied_relation env sigma (c,l) =
let open Context.Rel.Declaration in
let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in
let find_rel ty =
+ let ty = EConstr.of_constr ty in
let sigma, cl = Clenv.make_evar_clause env sigma ty in
+ let l = Miscops.map_bindings EConstr.of_constr l in
let sigma = Clenv.solve_evar_clause env sigma true cl l in
let { Clenv.cl_holes = holes; Clenv.cl_concl = t } = cl in
+ let t = EConstr.Unsafe.to_constr t in
let (equiv, c1, c2) = decompose_app_rel env sigma t in
let ty1 = Retyping.get_type_of env sigma (EConstr.of_constr c1) in
let ty2 = Retyping.get_type_of env sigma (EConstr.of_constr c2) in
@@ -517,7 +520,7 @@ let decompose_applied_relation env sigma (c,l) =
| None -> None
| Some sigma ->
let sort = sort_of_rel env sigma equiv in
- let args = Array.map_of_list (fun h -> h.Clenv.hole_evar) holes in
+ let args = Array.map_of_list (fun h -> EConstr.Unsafe.to_constr h.Clenv.hole_evar) holes in
let value = mkApp (c, args) in
Some (sigma, { prf=value;
car=ty1; rel = equiv; sort = Sorts.is_prop sort;
@@ -618,9 +621,10 @@ let solve_remaining_by env sigma holes by =
| Some tac ->
let map h =
if h.Clenv.hole_deps then None
- else
- let (evk, _) = destEvar (h.Clenv.hole_evar) in
+ else match EConstr.kind sigma h.Clenv.hole_evar with
+ | Evar (evk, _) ->
Some evk
+ | _ -> None
in
(** Only solve independent holes *)
let indep = List.map_filter map holes in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 77e91095f..ee6355736 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-module CVars = Vars
-
open CErrors
open Util
open Names
@@ -184,10 +182,12 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
| None -> raise Not_found
| Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
- let c' = EConstr.of_constr (CVars.subst_univs_level_constr subst c) in
- let t' = CVars.subst_univs_level_constr subst t' in
- let bs' = List.map (CVars.subst_univs_level_constr subst %> EConstr.of_constr) bs in
- let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in
+ let c = EConstr.of_constr c in
+ let c' = subst_univs_level_constr subst c in
+ let t' = EConstr.of_constr t' in
+ let t' = subst_univs_level_constr subst t' in
+ let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in
+ let h, _ = decompose_app_vect sigma t' in
ctx',(EConstr.of_constr h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
(Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
(n, Stack.zip sigma (t2,sk2))
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 142e430ff..7fe81c9a4 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -58,3 +58,16 @@ let map_red_expr_gen f g h = function
| CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o)
| Cbn flags -> Cbn (map_flags g flags)
| ExtraRedExpr _ | Red _ | Hnf as x -> x
+
+(** Mapping bindings *)
+
+let map_explicit_bindings f l =
+ let map (loc, hyp, x) = (loc, hyp, f x) in
+ List.map map l
+
+let map_bindings f = function
+| ImplicitBindings l -> ImplicitBindings (List.map f l)
+| ExplicitBindings expl -> ExplicitBindings (map_explicit_bindings f expl)
+| NoBindings -> NoBindings
+
+let map_with_bindings f (x, bl) = (f x, map_bindings f bl)
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index 337473a6f..f30dc1a4b 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -27,3 +27,8 @@ val intro_pattern_naming_eq :
val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
+
+(** Mapping bindings *)
+
+val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings
+val map_with_bindings : ('a -> 'b) -> 'a with_bindings -> 'b with_bindings
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0e0b80744..0dd615bfb 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1588,9 +1588,11 @@ let meta_instance sigma b =
if Metaset.is_empty fm then b.rebus
else
let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in
- instance sigma c_sigma (EConstr.of_constr b.rebus)
+ EConstr.of_constr (instance sigma c_sigma b.rebus)
-let nf_meta sigma c = meta_instance sigma (mk_freelisted c)
+let nf_meta sigma c =
+ let cl = mk_freelisted c in
+ EConstr.Unsafe.to_constr (meta_instance sigma { cl with rebus = EConstr.of_constr cl.rebus })
(* Instantiate metas that create beta/iota redexes *)
@@ -1652,7 +1654,7 @@ let meta_reducible_instance evd b =
| _ -> EConstr.map evd irec u
in
if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
- else EConstr.Unsafe.to_constr (irec (EConstr.of_constr b.rebus))
+ else irec b.rebus
let head_unfold_under_prod ts env sigma c =
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index c3b82729d..864b1a625 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -295,6 +295,6 @@ val whd_betaiota_deltazeta_for_iota_state :
state * Cst_stack.t
(** {6 Meta-related reduction functions } *)
-val meta_instance : evar_map -> constr freelisted -> constr
+val meta_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr
val nf_meta : evar_map -> constr -> constr
-val meta_reducible_instance : evar_map -> constr freelisted -> constr
+val meta_reducible_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index cf58a0b66..29697260f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -40,6 +40,7 @@ let meta_type evd mv =
let ty =
try Evd.meta_ftype evd mv
with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in
+ let ty = Evd.map_fl EConstr.of_constr ty in
meta_instance evd ty
let constant_type_knowing_parameters env sigma cst jl =
@@ -256,7 +257,7 @@ let rec execute env evdref cstr =
let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
match EConstr.kind !evdref cstr with
| Meta n ->
- { uj_val = cstr; uj_type = EConstr.of_constr (meta_type !evdref n) }
+ { uj_val = cstr; uj_type = meta_type !evdref n }
| Evar ev ->
let ty = EConstr.existential_type !evdref ev in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1fb414906..94a56b6e1 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -31,7 +31,7 @@ val e_sort_of : env -> evar_map ref -> EConstr.types -> sorts
val e_check : env -> evar_map ref -> EConstr.constr -> EConstr.types -> unit
(** Returns the instantiated type of a metavariable *)
-val meta_type : evar_map -> metavariable -> types
+val meta_type : evar_map -> metavariable -> EConstr.types
(** Solve existential variables using typing *)
val e_solve_evars : env -> evar_map ref -> EConstr.constr -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 483fefaf2..2b2069ec4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -617,10 +617,10 @@ let subst_defined_metas_evars sigma (bl,el) c =
in try Some (substrec c) with Not_found -> None
let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM tyN =
- match subst_defined_metas_evars sigma (metasubst,[]) (EConstr.of_constr tyM) with
+ match subst_defined_metas_evars sigma (metasubst,[]) tyM with
| None -> sigma
| Some m ->
- match subst_defined_metas_evars sigma (metasubst,[]) (EConstr.of_constr tyN) with
+ match subst_defined_metas_evars sigma (metasubst,[]) tyN with
| None -> sigma
| Some n ->
if is_ground_term sigma m && is_ground_term sigma n then
@@ -705,6 +705,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
(try
let tyM = Typing.meta_type sigma k in
let tyN = get_type_of curenv ~lax:true sigma cN in
+ let tyN = EConstr.of_constr tyN in
check_compatibility curenv CUMUL flags substn tyN tyM
with RetypeError _ ->
(* Renounce, maybe metas/evars prevents typing *) sigma)
@@ -724,6 +725,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
if opt.with_types && flags.check_applied_meta_types then
(try
let tyM = get_type_of curenv ~lax:true sigma cM in
+ let tyM = EConstr.of_constr tyM in
let tyN = Typing.meta_type sigma k in
check_compatibility curenv CUMUL flags substn tyM tyN
with RetypeError _ ->
@@ -977,6 +979,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
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 = EConstr.of_constr tyM in
+ let tyN = EConstr.of_constr tyN in
check_compatibility curenv CUMUL flags substn tyM tyN
with RetypeError _ ->
(* Renounce, maybe metas/evars prevents typing *) sigma
@@ -1265,7 +1269,7 @@ let w_coerce_to_type env evd c cty mvty =
let w_coerce env evd mv c =
let cty = get_type_of env evd c in
let mvty = Typing.meta_type evd mv in
- w_coerce_to_type env evd c (EConstr.of_constr cty) (EConstr.of_constr mvty)
+ w_coerce_to_type env evd c (EConstr.of_constr cty) mvty
let unify_to_type env sigma flags c status u =
let sigma, c = refresh_universes (Some false) env sigma c in
@@ -1275,6 +1279,7 @@ let unify_to_type env sigma flags c status u =
let unify_type env sigma flags mv status c =
let mvty = Typing.meta_type sigma mv in
+ let mvty = EConstr.Unsafe.to_constr mvty in
let mvty = nf_meta sigma mvty in
unify_to_type env sigma
(set_flags_for_type flags)
@@ -1923,7 +1928,6 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
let flags = { flags with core_unify_flags = flags.subterm_unify_flags } in
let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
let typp = Typing.meta_type evd' p in
- let typp = EConstr.of_constr typp in
let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in
let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in
if not b then
@@ -1942,7 +1946,7 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
let typp = Typing.meta_type evd p in
- let evd, pred = abstract_list_all_with_dependencies env evd (EConstr.of_constr typp) typ oplist in
+ let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in
let pred = EConstr.of_constr pred in
w_merge env false flags.merge_unify_flags
(evd,[p,pred,(Conv,TypeProcessed)],[])
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 67ed5daaa..3e3889cbb 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -12,11 +12,12 @@ open Util
open Names
open Nameops
open Term
-open Vars
open Termops
open Namegen
open Environ
open Evd
+open EConstr
+open Vars
open Reduction
open Reductionops
open Tacred
@@ -29,7 +30,7 @@ open Sigma.Notations
(* Abbreviations *)
let pf_env = Refiner.pf_env
-let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma (EConstr.of_constr c)
+let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c
(******************************************************************)
(* Clausal environments *)
@@ -43,12 +44,6 @@ type clausenv = {
let cl_env ce = ce.env
let cl_sigma ce = ce.evd
-let map_clenv sub clenv =
- { templval = map_fl sub clenv.templval;
- templtyp = map_fl sub clenv.templtyp;
- evd = cmap sub clenv.evd;
- env = clenv.env }
-
let clenv_nf_meta clenv c = nf_meta clenv.evd c
let clenv_term clenv c = meta_instance clenv.evd c
let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
@@ -56,30 +51,34 @@ let clenv_value clenv = meta_instance clenv.evd clenv.templval
let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
let refresh_undefined_univs clenv =
- match kind_of_term clenv.templval.rebus with
+ match EConstr.kind clenv.evd clenv.templval.rebus with
| Var _ -> clenv, Univ.empty_level_subst
- | App (f, args) when isVar f -> clenv, Univ.empty_level_subst
+ | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst
| _ ->
let evd', subst = Evd.refresh_undefined_universes clenv.evd in
let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
{ clenv with evd = evd'; templval = map_freelisted clenv.templval;
templtyp = map_freelisted clenv.templtyp }, subst
-let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
+let clenv_hnf_constr ce t = EConstr.of_constr (hnf_constr (cl_env ce) (cl_sigma ce) t)
-let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) (EConstr.of_constr c)
+let clenv_get_type_of ce c = EConstr.of_constr (Retyping.get_type_of (cl_env ce) (cl_sigma ce) c)
exception NotExtensibleClause
+let mk_freelisted c =
+ map_fl EConstr.of_constr (mk_freelisted (EConstr.Unsafe.to_constr c))
+
let clenv_push_prod cl =
- let typ = whd_all (cl_env cl) (cl_sigma cl) (EConstr.of_constr (clenv_type cl)) in
- let rec clrec typ = match kind_of_term typ with
+ let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+ let typ = EConstr.of_constr typ in
+ let rec clrec typ = match EConstr.kind cl.evd typ with
| Cast (t,_,_) -> clrec t
| Prod (na,t,u) ->
let mv = new_meta () in
- let dep = not (EConstr.Vars.noccurn (cl_sigma cl) 1 (EConstr.of_constr u)) in
+ let dep = not (noccurn (cl_sigma cl) 1 u) in
let na' = if dep then na else Anonymous in
- let e' = meta_declare mv t ~name:na' cl.evd in
+ let e' = meta_declare mv (EConstr.Unsafe.to_constr t) ~name:na' cl.evd in
let concl = if dep then subst1 (mkMeta mv) u else u in
let def = applist (cl.templval.rebus,[mkMeta mv]) in
{ templval = mk_freelisted def;
@@ -103,14 +102,17 @@ let clenv_push_prod cl =
and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
let clenv_environments evd bound t =
+ let open EConstr in
+ let open Vars in
let rec clrec (e,metas) n t =
- match n, kind_of_term t with
+ match n, EConstr.kind evd t with
| (Some 0, _) -> (e, List.rev metas, t)
| (n, Cast (t,_,_)) -> clrec (e,metas) n t
| (n, Prod (na,t1,t2)) ->
let mv = new_meta () in
- let dep = not (noccurn 1 t2) in
+ let dep = not (noccurn evd 1 t2) in
let na' = if dep then na else Anonymous in
+ let t1 = EConstr.Unsafe.to_constr t1 in
let e' = meta_declare mv t1 ~name:na' e in
clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
(if dep then (subst1 (mkMeta mv) t2) else t2)
@@ -132,7 +134,7 @@ let mk_clenv_from_n gls n (c,cty) =
let mk_clenv_from gls = mk_clenv_from_n gls None
-let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
+let mk_clenv_type_of gls t = mk_clenv_from gls (t,EConstr.of_constr (pf_type_of gls t))
(******************************************************************)
@@ -168,13 +170,13 @@ let clenv_assign mv rhs clenv =
error "clenv_assign: circularity in unification";
try
if meta_defined clenv.evd mv then
- if not (Term.eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
+ if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then
error_incompatible_inst clenv mv
else
clenv
else
let st = (Conv,TypeNotProcessed) in
- {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
+ {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd}
with Not_found ->
error "clenv_assign: undefined meta"
@@ -219,7 +221,7 @@ let clenv_assign mv rhs clenv =
*)
let clenv_metas_in_type_of_meta evd mv =
- (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
+ (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas
let dependent_in_type_of_metas clenv mvs =
List.fold_right
@@ -257,15 +259,14 @@ let clenv_dependent ce = clenv_dependent_gen false ce
let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
{ clenv with
- evd = w_unify ~flags clenv.env clenv.evd cv_pb (EConstr.of_constr t1) (EConstr.of_constr t2) }
+ evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
{ clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
let concl = Goal.V82.concl clenv.evd (sig_it gl) in
- let concl = EConstr.Unsafe.to_constr concl in
- if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr clenv.templtyp.rebus)))) then
+ if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd clenv.templtyp.rebus))))) then
clenv_unify CUMUL ~flags (clenv_type clenv) concl
(clenv_unify_meta_types ~flags clenv)
else
@@ -275,23 +276,19 @@ let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
let adjust_meta_source evd mv = function
| loc,Evar_kinds.VarInstance id ->
let rec match_name c l =
- match kind_of_term c, l with
- | Lambda (Name id,_,c), a::l when Constr.equal a (mkMeta mv) -> Some id
+ match EConstr.kind evd c, l with
+ | Lambda (Name id,_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id
| Lambda (_,_,c), a::l -> match_name c l
| _ -> None in
(* This is very ad hoc code so that an evar inherits the name of the binder
in situations like "ex_intro (fun x => P) ?ev p" *)
let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) ->
if Metaset.mem mv t.freemetas then
- let f,l = decompose_app t.rebus in
- match kind_of_term f with
+ let f,l = decompose_app evd (EConstr.of_constr t.rebus) in
+ match EConstr.kind evd f with
| Meta mv'' ->
(match meta_opt_fvalue evd mv'' with
- | Some (c,_) -> match_name c.rebus l
- | None -> None)
- | Evar ev ->
- (match existential_opt_value evd ev with
- | Some c -> match_name c l
+ | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l
| None -> None)
| _ -> None
else None in
@@ -333,13 +330,14 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
let ty = clenv_meta_type clenv mv in
(* Postpone the evar-ization if dependent on another meta *)
(* This assumes no cycle in the dependencies - is it correct ? *)
- if occur_meta clenv.evd (EConstr.of_constr ty) then fold clenv (mvs@[mv])
+ if occur_meta clenv.evd ty then fold clenv (mvs@[mv])
else
let src = evar_source_of_meta mv clenv.evd in
let src = adjust_meta_source clenv.evd mv src in
let evd = Sigma.Unsafe.of_evar_map clenv.evd in
- let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src (EConstr.of_constr ty) in
+ let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in
let evd = Sigma.to_evar_map evd in
+ let evar = EConstr.of_constr evar in
let clenv = clenv_assign mv evar {clenv with evd=evd} in
fold clenv mvs in
fold clenv dep_mvs
@@ -405,7 +403,7 @@ type arg_bindings = constr explicit_bindings
* of cval, ctyp. *)
let clenv_independent clenv =
- let mvs = collect_metas clenv.evd (EConstr.of_constr (clenv_value clenv)) in
+ let mvs = collect_metas clenv.evd (clenv_value clenv) in
let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in
List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
@@ -483,15 +481,13 @@ let error_already_defined b =
(str "Position " ++ int n ++ str" already defined.")
let clenv_unify_binding_type clenv c t u =
- let u = EConstr.of_constr u in
- if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then
+ if isMeta clenv.evd (EConstr.of_constr (fst (decompose_app_vect clenv.evd (EConstr.of_constr (whd_nored clenv.evd u))))) then
(* Not enough information to know if some subtyping is needed *)
CoerceToType, clenv, c
else
(* Enough information so as to try a coercion now *)
try
- let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd (EConstr.of_constr c) (EConstr.of_constr t) u in
- let c = EConstr.Unsafe.to_constr c in
+ let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
TypeProcessed, { clenv with evd = evd }, c
with
| PretypeError (_,_,ActualTypeNotCoercible (_,_,
@@ -501,9 +497,11 @@ let clenv_unify_binding_type clenv c t u =
TypeNotProcessed, clenv, c
let clenv_assign_binding clenv k c =
- let k_typ = clenv_hnf_constr clenv (EConstr.of_constr (clenv_meta_type clenv k)) in
- let c_typ = nf_betaiota clenv.evd (EConstr.of_constr (clenv_get_type_of clenv c)) in
+ let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
+ let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
+ let c_typ = EConstr.of_constr c_typ in
let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
+ let c = EConstr.Unsafe.to_constr c in
{ clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
let clenv_match_args bl clenv =
@@ -516,7 +514,7 @@ let clenv_match_args bl clenv =
(fun clenv (loc,b,c) ->
let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
- if Term.eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
+ if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
else error_already_defined b
else
clenv_assign_binding clenv k c)
@@ -525,7 +523,7 @@ let clenv_match_args bl clenv =
exception NoSuchBinding
let clenv_constrain_last_binding c clenv =
- let all_mvs = collect_metas clenv.evd (EConstr.of_constr clenv.templval.rebus) in
+ let all_mvs = collect_metas clenv.evd clenv.templval.rebus in
let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in
clenv_assign_binding clenv k c
@@ -560,8 +558,9 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
let clause = mk_clenv_from_env env sigma n (c,t) in
clenv_constrain_dep_args hyps_only largs clause
| ExplicitBindings lbind ->
+ let t = EConstr.of_constr (rename_bound_vars_as_displayed [] [] (EConstr.Unsafe.to_constr t)) in
let clause = mk_clenv_from_env env sigma n
- (c,rename_bound_vars_as_displayed [] [] t)
+ (c, t)
in clenv_match_args lbind clause
| NoBindings ->
mk_clenv_from_env env sigma n (c,t)
@@ -579,43 +578,49 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
(* Pretty-print *)
let pr_clenv clenv =
+ let inj = EConstr.Unsafe.to_constr in
h 0
- (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
- str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
+ (str"TEMPL: " ++ print_constr (inj clenv.templval.rebus) ++
+ str" : " ++ print_constr (inj clenv.templtyp.rebus) ++ fnl () ++
pr_evar_map (Some 2) clenv.evd)
(****************************************************************)
(** Evar version of mk_clenv *)
type hole = {
- hole_evar : constr;
- hole_type : types;
+ hole_evar : EConstr.constr;
+ hole_type : EConstr.types;
hole_deps : bool;
hole_name : Name.t;
}
type clause = {
cl_holes : hole list;
- cl_concl : types;
+ cl_concl : EConstr.types;
}
let make_evar_clause env sigma ?len t =
+ let open EConstr in
+ let open Vars in
let bound = match len with
| None -> -1
| Some n -> assert (0 <= n); n
in
(** FIXME: do the renaming online *)
+ let t = EConstr.Unsafe.to_constr t in
let t = rename_bound_vars_as_displayed [] [] t in
+ let t = EConstr.of_constr t in
let rec clrec (sigma, holes) n t =
if n = 0 then (sigma, holes, t)
- else match kind_of_term t with
+ else match EConstr.kind sigma t with
| Cast (t, _, _) -> clrec (sigma, holes) n t
| Prod (na, t1, t2) ->
let store = Typeclasses.set_resolvable Evd.Store.empty false in
let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma (ev, sigma, _) = new_evar ~store env sigma (EConstr.of_constr t1) in
+ let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
let sigma = Sigma.to_evar_map sigma in
- let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in
+ let ev = EConstr.of_constr ev in
+ let dep = not (noccurn sigma 1 t2) in
let hole = {
hole_evar = ev;
hole_type = t1;
@@ -670,26 +675,28 @@ let evar_of_binder holes = function
user_err (str "No such binder.")
let define_with_type sigma env ev c =
- let c = EConstr.of_constr c in
- let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in
+ let open EConstr in
+ let t = Retyping.get_type_of env sigma ev in
+ let t = EConstr.of_constr t in
let ty = Retyping.get_type_of env sigma c in
let ty = EConstr.of_constr ty in
let j = Environ.make_judge c ty in
- let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in
- let (ev, _) = destEvar ev in
+ let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
+ let (ev, _) = destEvar sigma ev in
let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
sigma
let solve_evar_clause env sigma hyp_only clause = function
| NoBindings -> sigma
| ImplicitBindings largs ->
+ let open EConstr in
let fold holes h =
if h.hole_deps then
(** Some subsequent term uses the hole *)
- let (ev, _) = destEvar h.hole_evar in
- let is_dep hole = occur_evar sigma ev (EConstr.of_constr hole.hole_type) in
+ let (ev, _) = destEvar sigma h.hole_evar in
+ let is_dep hole = occur_evar sigma ev hole.hole_type in
let in_hyp = List.exists is_dep holes in
- let in_ccl = occur_evar sigma ev (EConstr.of_constr clause.cl_concl) in
+ let in_ccl = occur_evar sigma ev clause.cl_concl in
let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in
let h = { h with hole_deps = dep } in
h :: holes
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index e9236b1da..e4f6f9a91 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -14,6 +14,7 @@ open Names
open Term
open Environ
open Evd
+open EConstr
open Unification
open Misctypes
@@ -28,8 +29,6 @@ type clausenv = {
templtyp : constr freelisted (** its type *)}
-val map_clenv : (constr -> constr) -> clausenv -> clausenv
-
(** subject of clenv (instantiated) *)
val clenv_value : clausenv -> constr
@@ -37,16 +36,16 @@ val clenv_value : clausenv -> constr
val clenv_type : clausenv -> types
(** substitute resolved metas *)
-val clenv_nf_meta : clausenv -> constr -> constr
+val clenv_nf_meta : clausenv -> Constr.constr -> Constr.constr
(** type of a meta in clenv context *)
val clenv_meta_type : clausenv -> metavariable -> types
-val mk_clenv_from : Goal.goal sigma -> constr * types -> clausenv
+val mk_clenv_from : Goal.goal sigma -> EConstr.constr * EConstr.types -> clausenv
val mk_clenv_from_n :
- Goal.goal sigma -> int option -> constr * types -> clausenv
-val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
-val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
+ Goal.goal sigma -> int option -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_type_of : Goal.goal sigma -> EConstr.constr -> clausenv
+val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
(** Refresh the universes in a clenv *)
val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
@@ -92,18 +91,18 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
the optional int tells how many prods of the lemma have to be used
use all of them if None *)
val make_clenv_binding_env_apply :
- env -> evar_map -> int option -> constr * constr -> constr bindings ->
+ env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
clausenv
val make_clenv_binding_apply :
- env -> evar_map -> int option -> constr * constr -> constr bindings ->
+ env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
clausenv
val make_clenv_binding_env :
- env -> evar_map -> constr * constr -> constr bindings -> clausenv
+ env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
val make_clenv_binding :
- env -> evar_map -> constr * constr -> constr bindings -> clausenv
+ env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv
(** if the clause is a product, add an extra meta for this product *)
exception NotExtensibleClause
@@ -134,9 +133,9 @@ val pr_clenv : clausenv -> Pp.std_ppcmds
*)
type hole = {
- hole_evar : constr;
+ hole_evar : EConstr.constr;
(** The hole itself. Guaranteed to be an evar. *)
- hole_type : types;
+ hole_type : EConstr.types;
(** Type of the hole in the current environment. *)
hole_deps : bool;
(** Whether the remainder of the clause was dependent in the hole. Note that
@@ -148,10 +147,10 @@ type hole = {
type clause = {
cl_holes : hole list;
- cl_concl : types;
+ cl_concl : EConstr.types;
}
-val make_evar_clause : env -> evar_map -> ?len:int -> types ->
+val make_evar_clause : env -> evar_map -> ?len:int -> EConstr.types ->
(evar_map * clause)
(** An evar version of {!make_clenv_binding}. Given a type [t],
[evar_environments env sigma ~len t bl] tries to eliminate at most [len]
@@ -159,7 +158,7 @@ val make_evar_clause : env -> evar_map -> ?len:int -> types ->
type together with the list of holes generated. Assumes that [t] is
well-typed in the environment. *)
-val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings ->
+val solve_evar_clause : env -> evar_map -> bool -> clause -> EConstr.constr bindings ->
evar_map
(** [solve_evar_clause env sigma hyps cl bl] tries to solve the holes contained
in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 5b9322bfe..539b1bcb2 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -11,6 +11,7 @@ open Names
open Term
open Termops
open Evd
+open EConstr
open Refiner
open Logic
open Reduction
@@ -26,19 +27,19 @@ open Proofview.Notations
let clenv_cast_meta clenv =
let rec crec u =
- match kind_of_term u with
+ match EConstr.kind clenv.evd u with
| App _ | Case _ -> crec_hd u
- | Cast (c,_,_) when isMeta c -> u
+ | Cast (c,_,_) when isMeta clenv.evd c -> u
| Proj (p, c) -> mkProj (p, crec_hd c)
- | _ -> map_constr crec u
+ | _ -> EConstr.map clenv.evd crec u
and crec_hd u =
- match kind_of_term (strip_outer_cast clenv.evd (EConstr.of_constr u)) with
+ match EConstr.kind clenv.evd (EConstr.of_constr (strip_outer_cast clenv.evd u)) with
| Meta mv ->
(try
let b = Typing.meta_type clenv.evd mv in
- assert (not (occur_meta clenv.evd (EConstr.of_constr b)));
- if occur_meta clenv.evd (EConstr.of_constr b) then u
+ assert (not (occur_meta clenv.evd b));
+ if occur_meta clenv.evd b then u
else mkCast (mkMeta mv, DEFAULTcast, b)
with Not_found -> u)
| App(f,args) -> mkApp (crec_hd f, Array.map crec args)
@@ -95,7 +96,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv =
let clenv = { clenv with evd = evd' } in
tclTHEN
(tclEVARS (Evd.clear_metas evd'))
- (refine_no_check (EConstr.of_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl
+ (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
end
open Unification
@@ -143,7 +144,7 @@ let unify ?(flags=fail_quick_unif_flags) m =
let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
let evd = clear_metas (Tacmach.New.project gl) in
try
- let evd' = w_unify env evd CONV ~flags (EConstr.of_constr m) (EConstr.of_constr n) in
+ let evd' = w_unify env evd CONV ~flags m (EConstr.of_constr n) in
Proofview.Unsafe.tclEVARSADVANCE evd'
with e when CErrors.noncritical e -> Proofview.tclZERO e
end }
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 8a096b645..5b7164705 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -10,6 +10,7 @@
open Term
open Clenv
+open EConstr
open Unification
open Misctypes
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7462b8d85..2b654f563 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -84,11 +84,12 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
(** Refresh the instance of the hint *)
let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
let map c = Vars.subst_univs_level_constr subst c in
+ let emap c = EConstr.Vars.subst_univs_level_constr subst c in
let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
(** Only metas are mentioning the old universes. *)
let clenv = {
- templval = Evd.map_fl map clenv.templval;
- templtyp = Evd.map_fl map clenv.templtyp;
+ templval = Evd.map_fl emap clenv.templval;
+ templtyp = Evd.map_fl emap clenv.templtyp;
evd = Evd.map_metas map evd;
env = Proofview.Goal.env gl;
} in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 80b9ec06e..b567344c9 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -257,12 +257,12 @@ type hypinfo = {
let decompose_applied_relation metas env sigma c ctype left2right =
let find_rel ty =
- let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
+ let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,EConstr.of_constr ty) in
let eqclause =
if metas then eqclause
else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
in
- let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
+ let (equiv, args) = decompose_app (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z ->
@@ -276,7 +276,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
in
(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
(* else *)
- Some { hyp_cl=eqclause; hyp_prf=(Clenv.clenv_value eqclause); hyp_ty = ty;
+ Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty;
hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others);
hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; }
with Not_found -> None
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a2699ba8d..a8768b6ed 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -227,6 +227,7 @@ let e_give_exact flags poly (c,clenv) gl =
else c, gl
in
let t1 = pf_unsafe_type_of gl (EConstr.of_constr c) in
+ let t1 = EConstr.of_constr t1 in
Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
@@ -247,6 +248,7 @@ let unify_resolve_refine poly flags =
{ enter = begin fun gls ((c, t, ctx),n,clenv) ->
let env = Proofview.Goal.env gls in
let concl = Proofview.Goal.concl gls in
+ let concl = EConstr.of_constr concl in
Refine.refine ~unsafe:true { Sigma.run = fun sigma ->
let sigma = Sigma.to_evar_map sigma in
let sigma, term, ty =
@@ -259,17 +261,20 @@ let unify_resolve_refine poly flags =
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
sigma, c, t
in
+ let open EConstr in
+ let ty = EConstr.of_constr ty in
+ let term = EConstr.of_constr term in
let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
- let term = applistc term (List.map (fun x -> x.hole_evar) cl.cl_holes) in
+ let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
let sigma' =
let evdref = ref sigma' in
if not (Evarconv.e_cumul env ~ts:flags.core_unify_flags.modulo_delta
- evdref (EConstr.of_constr cl.cl_concl) (EConstr.of_constr concl)) then
- Type_errors.error_actual_type env
+ evdref cl.cl_concl concl) then
+ Pretype_errors.error_actual_type_core env sigma'
{Environ.uj_val = term; Environ.uj_type = cl.cl_concl}
concl;
!evdref
- in Sigma.here (EConstr.of_constr term) (Sigma.Unsafe.of_evar_map sigma') }
+ in Sigma.here term (Sigma.Unsafe.of_evar_map sigma') }
end }
(** Dealing with goals of the form A -> B and hints of the form
@@ -279,9 +284,11 @@ let clenv_of_prods poly nprods (c, clenv) gl =
let (c, _, _) = c in
if poly || Int.equal nprods 0 then Some (None, clenv)
else
+ let c = EConstr.of_constr c in
let sigma = Tacmach.New.project gl in
- let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma (EConstr.of_constr c) in
- let diff = nb_prod sigma (EConstr.of_constr ty) - nprods in
+ let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
+ let ty = EConstr.of_constr ty in
+ let diff = nb_prod sigma ty - nprods in
if Pervasives.(>=) diff 0 then
(* Was Some clenv... *)
Some (Some diff,
@@ -1515,7 +1522,7 @@ let autoapply c i gl =
let flags = auto_unif_flags Evar.Set.empty
(Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
let cty = pf_unsafe_type_of gl (EConstr.of_constr c) in
- let ce = mk_clenv_from gl (c,cty) in
+ let ce = mk_clenv_from gl (EConstr.of_constr c,EConstr.of_constr cty) in
let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl
((c,cty,Univ.ContextSet.empty),0,ce) } in
Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2fad4fcf7..7b07c9309 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -31,9 +31,10 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state
let e_give_exact ?(flags=eauto_unif_flags) c =
Proofview.Goal.enter { enter = begin fun gl ->
let t1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
+ let t1 = EConstr.of_constr t1 in
let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
let sigma = Tacmach.New.project gl in
- if occur_existential sigma (EConstr.of_constr t1) || occur_existential sigma (EConstr.of_constr t2) then
+ if occur_existential sigma t1 || occur_existential sigma (EConstr.of_constr t2) then
Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
else exact_check c
end }
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ad80d2d1f..fbf461f6f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -144,7 +144,7 @@ let freeze_initial_evars sigma flags clause =
(* We take evars of the type: this may include old evars! For excluding *)
(* all old evars, including the ones occurring in the rewriting lemma, *)
(* we would have to take the clenv_value *)
- let newevars = Evd.evars_of_term (clenv_type clause) in
+ let newevars = Evd.evars_of_term (EConstr.Unsafe.to_constr (clenv_type clause)) in
let evars =
fold_undefined (fun evk _ evars ->
if Evar.Set.mem evk newevars then evars
@@ -165,8 +165,11 @@ let side_tac tac sidetac =
let instantiate_lemma_all frzevars gl c ty l l2r concl =
let env = Proofview.Goal.env gl in
+ let c = EConstr.of_constr c in
+ let ty = EConstr.of_constr ty in
+ let l = Miscops.map_bindings EConstr.of_constr l in
let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
- let (equiv, args) = decompose_appvect (Clenv.clenv_type eqclause) in
+ let (equiv, args) = decompose_appvect (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
let arglen = Array.length args in
let () = if arglen < 2 then error "The term provided is not an applied relation." in
let c1 = args.(arglen - 2) in
@@ -181,8 +184,11 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
in List.map try_occ occs
let instantiate_lemma gl c ty l l2r concl =
- let sigma, ct = pf_type_of gl (EConstr.of_constr c) in
+ let c = EConstr.of_constr c in
+ let sigma, ct = pf_type_of gl c in
let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma (EConstr.of_constr ct)) with UserError _ -> ct in
+ let t = EConstr.of_constr t in
+ let l = Miscops.map_bindings EConstr.of_constr l in
let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
[eqclause]
@@ -975,9 +981,11 @@ let eq_baseid = Id.of_string "e"
let apply_on_clause (f,t) clause =
let sigma = clause.evd in
+ let f = EConstr.of_constr f in
+ let t = EConstr.of_constr t in
let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
let argmv =
- (match kind_of_term (last_arg f_clause.evd (EConstr.of_constr f_clause.templval.Evd.rebus)) with
+ (match kind_of_term (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
| Meta mv -> mv
| _ -> user_err (str "Ill-formed clause applicator.")) in
clenv_fchain ~with_univs:false argmv f_clause clause
@@ -992,7 +1000,6 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
let pf_ty = mkArrow eqn absurd_term in
let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
- let pf = EConstr.of_constr pf in
Proofview.Unsafe.tclEVARS sigma <*>
Proofview.tclEFFECTS eff <*>
tclTHENS (assert_after Anonymous absurd_term)
@@ -1011,13 +1018,17 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let onEquality with_evars tac (c,lbindc) =
Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let c = EConstr.of_constr c in
+ let lbindc = Miscops.map_bindings EConstr.of_constr lbindc in
let type_of = pf_unsafe_type_of gl in
let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
- let t = type_of (EConstr.of_constr c) in
+ let t = type_of c in
let t' = try snd (reduce_to_quantified_ind (EConstr.of_constr t)) with UserError _ -> t in
+ let t' = EConstr.of_constr t' in
let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
let eqn = clenv_type eq_clause' in
+ let eqn = EConstr.Unsafe.to_constr eqn in
let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
tclTHEN
(Proofview.Unsafe.tclEVARS eq_clause'.evd)
@@ -1371,7 +1382,8 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
let sigma, pf_typ = Typing.type_of env sigma (EConstr.of_constr pf) in
let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
let pf = Clenvtac.clenv_value_cast_meta inj_clause in
- let ty = simplify_args env sigma (clenv_type inj_clause) in
+ let ty = simplify_args env sigma (EConstr.Unsafe.to_constr (clenv_type inj_clause)) in
+ let pf = EConstr.Unsafe.to_constr pf in
evdref := sigma;
Some (pf, ty)
with Failure _ -> None
@@ -1405,7 +1417,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
tclZEROMSG (str"Nothing to inject.")
| Inr posns ->
inject_at_positions env sigma l2r u eq_clause posns
- (tac (clenv_value eq_clause))
+ (tac (EConstr.Unsafe.to_constr (clenv_value eq_clause)))
let get_previous_hyp_position id gl =
let rec aux dest = function
@@ -1464,10 +1476,10 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
| Inl (cpath, (_,dirn), _) ->
discr_positions env sigma u clause cpath dirn
| Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
- ntac (clenv_value clause) 0
+ ntac (EConstr.Unsafe.to_constr (clenv_value clause)) 0
| Inr posns ->
inject_at_positions env sigma true u clause posns
- (ntac (clenv_value clause))
+ (ntac (EConstr.Unsafe.to_constr (clenv_value clause)))
end }
let dEqThen with_evars ntac = function
@@ -1478,9 +1490,11 @@ let dEq with_evars =
dEqThen with_evars (fun clear_flag c x ->
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
-let intro_decomp_eq tac data cl =
+let intro_decomp_eq tac data (c, t) =
Proofview.Goal.enter { enter = begin fun gl ->
- let cl = pf_apply make_clenv_binding gl cl NoBindings in
+ let c = EConstr.of_constr c in
+ let t = EConstr.of_constr t in
+ let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
decompEqThen (fun _ -> tac) data cl
end }
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 57358bb76..ea95fb1ad 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -276,9 +276,11 @@ let strip_params env c =
let instantiate_hint env sigma p =
let mk_clenv (c, cty, ctx) =
let sigma = Evd.merge_context_set univ_flexible sigma ctx in
+ let c = EConstr.of_constr c in
+ let cty = EConstr.of_constr cty in
let cl = mk_clenv_from_env env sigma None (c,cty) in
{cl with templval =
- { cl.templval with rebus = strip_params env cl.templval.rebus };
+ { cl.templval with rebus = EConstr.of_constr (strip_params env (EConstr.Unsafe.to_constr cl.templval.rebus)) };
env = empty_env}
in
let code = match p.code.obj with
@@ -765,9 +767,9 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
match kind_of_term cty with
| Prod _ ->
let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
- let ce = mk_clenv_from_env env sigma' None (c,cty) in
+ let ce = mk_clenv_from_env env sigma' None (EConstr.of_constr c,EConstr.of_constr cty) in
let c' = clenv_type (* ~reduce:false *) ce in
- let pat = Patternops.pattern_of_constr env ce.evd (EConstr.of_constr c') in
+ let pat = Patternops.pattern_of_constr env ce.evd c' in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry" in
@@ -912,10 +914,10 @@ let make_trivial env sigma poly ?(name=PathAny) r =
let sigma = Evd.merge_context_set univ_flexible sigma ctx in
let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma (EConstr.of_constr c))) in
let hd = head_of_constr_reference sigma (EConstr.of_constr (head_constr sigma t)) in
- let ce = mk_clenv_from_env env sigma None (c,t) in
+ let ce = mk_clenv_from_env env sigma None (EConstr.of_constr c,EConstr.of_constr t) in
(Some hd, { pri=1;
poly = poly;
- pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.of_constr (clenv_type ce)));
+ pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
name = name;
db = None;
secvars = secvars_of_constr env c;
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 85910355e..16a048af8 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -258,8 +258,8 @@ let add_inversion_lemma_exn na com comsort bool tac =
let lemInv id c gls =
try
- let clause = mk_clenv_type_of gls c in
- let clause = clenv_constrain_last_binding (mkVar id) clause in
+ let clause = mk_clenv_type_of gls (EConstr.of_constr 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 ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 02909243d..459947051 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -622,20 +622,22 @@ module New = struct
(* c should be of type A1->.. An->B with B an inductive definition *)
let general_elim_then_using mk_elim
isrec allnames tac predicate ind (c, t) =
+ let c = EConstr.of_constr c in
+ let t = EConstr.of_constr t in
Proofview.Goal.nf_enter { enter = begin fun gl ->
let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Proofview.Goal.nf_enter { enter = begin fun gl ->
let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
(* applying elimination_scheme just a little modified *)
- let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elim))) gl in
+ let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (EConstr.of_constr elim,EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elim)))) gl in
let indmv =
- match kind_of_term (last_arg elimclause.evd (EConstr.of_constr elimclause.templval.Evd.rebus)) with
+ match kind_of_term (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
| Meta mv -> mv
| _ -> anomaly (str"elimination")
in
let pmv =
- let p, _ = decompose_app elimclause.templtyp.Evd.rebus in
+ let p, _ = decompose_app (EConstr.Unsafe.to_constr elimclause.templtyp.Evd.rebus) in
match kind_of_term p with
| Meta p -> p
| _ ->
@@ -655,11 +657,11 @@ module New = struct
let elimclause' =
match predicate with
| None -> elimclause'
- | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
+ | Some p -> clenv_unify ~flags Reduction.CONV (EConstr.mkMeta pmv) (EConstr.of_constr p) elimclause'
in
let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in
let after_tac i =
- let (hd,largs) = decompose_app clenv'.templtyp.Evd.rebus in
+ let (hd,largs) = decompose_app (EConstr.Unsafe.to_constr clenv'.templtyp.Evd.rebus) in
let ba = { branchsign = branchsigns.(i);
branchnames = brnames.(i);
nassums = List.length branchsigns.(i);
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b9a219a2c..f262aefa7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1301,11 +1301,11 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
else clenv
in
let new_hyp_typ = clenv_type clenv in
+ let new_hyp_typ = EConstr.Unsafe.to_constr new_hyp_typ in
if not with_evars then check_unresolved_evars_of_metas sigma0 clenv;
if not with_evars && occur_meta clenv.evd (EConstr.of_constr new_hyp_typ) then
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
- let new_hyp_prf = EConstr.of_constr new_hyp_prf in
let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in
let naming = NamingMustBe (dloc,targetid) in
let with_clear = do_replace (Some id) naming in
@@ -1396,9 +1396,12 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let elim = contract_letin_in_lam_header elim in
+ let bindings = Miscops.map_bindings EConstr.of_constr bindings in
+ let elim = EConstr.of_constr elim in
+ let elimty = EConstr.of_constr elimty in
let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
let indmv =
- (match kind_of_term (nth_arg i elimclause.templval.rebus) with
+ (match kind_of_term (nth_arg i (EConstr.Unsafe.to_constr elimclause.templval.rebus)) with
| Meta mv -> mv
| _ -> user_err ~hdr:"elimination_clause"
(str "The type of elimination clause is not well-formed."))
@@ -1438,8 +1441,10 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
let sigma = Tacmach.New.project gl in
let ct = Retyping.get_type_of env sigma (EConstr.of_constr c) in
let t = try snd (reduce_to_quantified_ind env sigma (EConstr.of_constr ct)) with UserError _ -> ct in
+ let t = EConstr.of_constr t in
let elimtac = elimination_clause_scheme with_evars in
- let indclause = make_clenv_binding env sigma (c, t) lbindc in
+ let lbindc = Miscops.map_bindings EConstr.of_constr lbindc in
+ let indclause = make_clenv_binding env sigma (EConstr.of_constr c, t) lbindc in
let sigma = meta_merge sigma (clear_metas indclause.evd) in
Proofview.Unsafe.tclEVARS sigma <*>
Tacticals.New.tclTHEN
@@ -1561,8 +1566,11 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let elim = contract_letin_in_lam_header elim in
+ let elim = EConstr.of_constr elim in
+ let elimty = EConstr.of_constr elimty in
+ let bindings = Miscops.map_bindings EConstr.of_constr bindings in
let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
- let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
+ let indmv = destMeta (nth_arg i (EConstr.Unsafe.to_constr elimclause.templval.rebus)) in
let hypmv =
try match List.remove Int.equal indmv (clenv_independent elimclause) with
| [a] -> a
@@ -1570,12 +1578,13 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
with Failure _ -> user_err ~hdr:"elimination_clause"
(str "The type of elimination clause is not well-formed.") in
let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
- let hyp = mkVar id in
- let hyp_typ = Retyping.get_type_of env sigma (EConstr.of_constr hyp) in
+ let hyp = EConstr.mkVar id in
+ let hyp_typ = Retyping.get_type_of env sigma hyp in
+ let hyp_typ = EConstr.of_constr hyp_typ in
let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
let new_hyp_typ = clenv_type elimclause'' in
- if Term.eq_constr hyp_typ new_hyp_typ then
+ if EConstr.eq_constr sigma hyp_typ new_hyp_typ then
user_err ~hdr:"general_rewrite_in"
(str "Nothing to rewrite in " ++ pr_id id ++ str".");
clenv_refine_in with_evars id id sigma elimclause''
@@ -1728,9 +1737,11 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
let thm_ty0 = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))) in
let try_apply thm_ty nprod =
try
- let n = nb_prod_modulo_zeta sigma (EConstr.of_constr thm_ty) - nprod in
+ let thm_ty = EConstr.of_constr thm_ty in
+ let n = nb_prod_modulo_zeta sigma thm_ty - nprod in
if n<0 then error "Applied theorem has not enough premisses.";
- let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
+ let lbind = Miscops.map_bindings EConstr.of_constr lbind in
+ let clause = make_clenv_binding_apply env sigma (Some n) (EConstr.of_constr c,thm_ty) lbind in
Clenvtac.res_pf clause ~with_evars ~flags
with exn when catchable_exception exn ->
Proofview.tclZERO exn
@@ -1851,7 +1862,9 @@ let progress_with_clause flags innerclause clause =
with Not_found -> error "Unable to unify."
let apply_in_once_main flags innerclause env sigma (d,lbind) =
- let thm = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma (EConstr.of_constr d))) in
+ let d = EConstr.of_constr d in
+ let thm = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma d)) in
+ let thm = EConstr.of_constr thm in
let rec aux clause =
try progress_with_clause flags innerclause clause
with e when CErrors.noncritical e ->
@@ -1859,6 +1872,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
try aux (clenv_push_prod clause)
with NotExtensibleClause -> iraise e
in
+ let lbind = Miscops.map_bindings EConstr.of_constr lbind in
aux (make_clenv_binding env sigma (d,thm) lbind)
let apply_in_once sidecond_first with_delta with_destruct with_evars naming
@@ -1870,7 +1884,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
let flags =
if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
let t' = Tacmach.New.pf_get_hyp_typ id gl in
- let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
+ let innerclause = mk_clenv_from_env env sigma (Some 0) (EConstr.mkVar id,EConstr.of_constr t') in
let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in
let rec aux idstoclear with_destruct c =
Proofview.Goal.enter { enter = begin fun gl ->
@@ -2939,10 +2953,12 @@ let specialize (c,lbind) ipat =
let sigma = Typeclasses.resolve_typeclasses env sigma in
sigma, nf_evar sigma c
else
- let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma (EConstr.of_constr c)) lbind in
+ let c = EConstr.of_constr c in
+ let lbind = Miscops.map_bindings EConstr.of_constr lbind in
+ let clause = make_clenv_binding env sigma (c,EConstr.of_constr (Retyping.get_type_of env sigma c)) lbind in
let flags = { (default_unify_flags ()) with resolve_evars = true } in
let clause = clenv_unify_meta_types ~flags clause in
- let (thd,tstack) = whd_nored_stack clause.evd (EConstr.of_constr (clenv_value clause)) in
+ let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
let rec chk = function
| [] -> []
| t::l -> if occur_meta clause.evd t then [] else EConstr.Unsafe.to_constr t :: chk l
@@ -4107,7 +4123,7 @@ let get_eliminator elim dep s gl =
of lid are parameters (first ones), the other are
arguments. Returns the clause obtained. *)
let recolle_clenv i params args elimclause gl =
- let _,arr = destApp elimclause.templval.rebus in
+ let _,arr = destApp (EConstr.Unsafe.to_constr elimclause.templval.rebus) in
let lindmv =
Array.map
(fun x ->
@@ -4132,6 +4148,8 @@ let recolle_clenv i params args elimclause gl =
(* from_n (Some 0) means that x should be taken "as is" without
trying to unify (which would lead to trying to apply it to
evars if y is a product). *)
+ let x = EConstr.of_constr x in
+ let y = EConstr.of_constr y in
let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from_n gl (Some 0) (x,y)) gl in
let elimclause' = clenv_fchain ~with_univs:false i acc indclause in
elimclause')
@@ -4149,6 +4167,9 @@ let induction_tac with_evars params indvars elim =
(* elimclause contains this: (elimc ?i ?j ?k...?l) *)
let elimc = contract_letin_in_lam_header elimc in
let elimc = mkCast (elimc, DEFAULTcast, elimt) in
+ let elimc = EConstr.of_constr elimc in
+ let elimt = EConstr.of_constr elimt in
+ let lbindelimc = Miscops.map_bindings EConstr.of_constr lbindelimc in
let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
(* elimclause' is built from elimclause by instanciating all args and params. *)
let elimclause' = recolle_clenv i params indvars elimclause gl in
@@ -4294,11 +4315,14 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
typ in
let rec find_clause typ =
try
+ let typ = EConstr.of_constr typ in
+ let c = EConstr.of_constr c in
+ let lbind = Miscops.map_bindings EConstr.of_constr lbind in
let indclause = make_clenv_binding env sigma (c,typ) lbind in
- if must_be_closed && occur_meta indclause.evd (EConstr.of_constr (clenv_value indclause)) then
+ if must_be_closed && occur_meta indclause.evd (clenv_value indclause) then
error "Need a fully applied argument.";
(* We lose the possibility of coercions in with-bindings *)
- let (sigma, c) = pose_all_metas_as_evars env indclause.evd (EConstr.of_constr (clenv_value indclause)) in
+ let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in
Sigma.Unsafe.of_pair (EConstr.Unsafe.to_constr c, sigma)
with e when catchable_exception e ->
try find_clause (try_red_product env sigma (EConstr.of_constr typ))
@@ -4308,13 +4332,15 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
let check_expected_type env sigma (elimc,bl) elimt =
(* Compute the expected template type of the term in case a using
clause is given *)
- let sign,_ = splay_prod env sigma (EConstr.of_constr elimt) in
+ let open EConstr in
+ let elimt = EConstr.of_constr elimt in
+ let sign,_ = splay_prod env sigma elimt in
let n = List.length sign in
if n == 0 then error "Scheme cannot be applied.";
let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
let sigma = solve_evar_clause env sigma true cl bl in
- let (_,u,_) = destProd cl.cl_concl in
- fun t -> Evarconv.e_cumul env (ref sigma) t (EConstr.of_constr u)
+ let (_,u,_) = destProd sigma cl.cl_concl in
+ fun t -> Evarconv.e_cumul env (ref sigma) t u
let check_enough_applied env sigma elim =
let sigma = Sigma.to_evar_map sigma in
@@ -4327,6 +4353,7 @@ let check_enough_applied env sigma elim =
| Some elimc ->
let elimt = Retyping.get_type_of env sigma (EConstr.of_constr (fst elimc)) in
let scheme = compute_elim_sig ~elimc elimt in
+ let elimc = Miscops.map_with_bindings EConstr.of_constr elimc in
match scheme.indref with
| None ->
(* in the absence of information, do not assume it may be
@@ -4607,12 +4634,13 @@ let simple_destruct = function
let elim_scheme_type elim t =
Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let elim = EConstr.of_constr elim in
let clause = Tacmach.New.of_old (fun gl -> mk_clenv_type_of gl elim) gl in
- match kind_of_term (last_arg clause.templval.rebus) with
+ match kind_of_term (last_arg (EConstr.Unsafe.to_constr clause.templval.rebus)) with
| Meta mv ->
let clause' =
(* t is inductive, then CUMUL or CONV is irrelevant *)
- clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t
+ clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL (EConstr.of_constr t)
(clenv_meta_type clause mv) clause in
Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
| _ -> anomaly (Pp.str "elim_scheme_type")
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 07:59:18 +0000