aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/eConstr.ml5
-rw-r--r--engine/eConstr.mli6
-rw-r--r--engine/evarutil.ml17
-rw-r--r--engine/evarutil.mli2
-rw-r--r--engine/termops.ml2
-rw-r--r--engine/termops.mli1
-rw-r--r--ltac/extratactics.ml418
-rw-r--r--ltac/rewrite.ml1
-rw-r--r--plugins/cc/cctac.ml3
-rw-r--r--plugins/fourier/fourierR.ml12
-rw-r--r--plugins/funind/functional_principles_proofs.ml10
-rw-r--r--plugins/funind/indfun_common.ml1
-rw-r--r--plugins/funind/invfun.ml10
-rw-r--r--plugins/funind/recdef.ml12
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/class_tactics.ml4
-rw-r--r--tactics/eqdecide.ml2
-rw-r--r--tactics/equality.ml304
-rw-r--r--tactics/equality.mli21
-rw-r--r--tactics/hints.ml2
-rw-r--r--tactics/inv.ml10
-rw-r--r--toplevel/auto_ind_decl.ml12
22 files changed, 241 insertions, 218 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 9e0a55a0d..1dd9d0c00 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -78,6 +78,8 @@ type cofixpoint = (t, t) pcofixpoint
type unsafe_judgment = (constr, types) Environ.punsafe_judgment
type unsafe_type_judgment = types Environ.punsafe_type_judgment
+let in_punivs a = (a, Univ.Instance.empty)
+
let mkProp = of_kind (Sort Sorts.prop)
let mkSet = of_kind (Sort Sorts.set)
let mkType u = of_kind (Sort (Sorts.Type u))
@@ -92,8 +94,11 @@ let mkLambda (na, t, c) = of_kind (Lambda (na, t, c))
let mkLetIn (na, b, t, c) = of_kind (LetIn (na, b, t, c))
let mkApp (f, arg) = of_kind (App (f, arg))
let mkConstU pc = of_kind (Const pc)
+let mkConst c = of_kind (Const (in_punivs c))
let mkIndU pi = of_kind (Ind pi)
+let mkInd i = of_kind (Ind (in_punivs i))
let mkConstructU pc = of_kind (Construct pc)
+let mkConstruct c = of_kind (Construct (in_punivs c))
let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
let mkFix f = of_kind (Fix f)
let mkCoFix f = of_kind (CoFix f)
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 15463a8f6..e6270fa78 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -62,12 +62,12 @@ val mkProd : Name.t * t * t -> t
val mkLambda : Name.t * t * t -> t
val mkLetIn : Name.t * t * t * t -> t
val mkApp : t * t array -> t
-(* val mkConst : constant -> t *)
+val mkConst : constant -> t
val mkConstU : pconstant -> t
val mkProj : (projection * t) -> t
-(* val mkInd : inductive -> t *)
+val mkInd : inductive -> t
val mkIndU : pinductive -> t
-(* val mkConstruct : constructor -> t *)
+val mkConstruct : constructor -> t
val mkConstructU : pconstructor -> t
(* val mkConstructUi : pinductive * int -> t *)
val mkCase : case_info * t * t * t array -> t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 4f40499d0..c2ad3c462 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -690,29 +690,26 @@ let rec advance sigma evk =
let undefined_evars_of_term evd t =
let rec evrec acc c =
- match kind_of_term c with
+ match EConstr.kind evd c with
| Evar (n, l) ->
- let acc = Array.fold_left evrec acc l in
- (try match (Evd.find evd n).evar_body with
- | Evar_empty -> Evar.Set.add n acc
- | Evar_defined c -> evrec acc c
- with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found"))
- | _ -> fold_constr evrec acc c
+ let acc = Evar.Set.add n acc in
+ Array.fold_left evrec acc l
+ | _ -> EConstr.fold evd evrec acc c
in
evrec Evar.Set.empty t
let undefined_evars_of_named_context evd nc =
Context.Named.fold_outside
- (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c)))
+ (NamedDecl.fold_constr (fun c s -> Evar.Set.union s (undefined_evars_of_term evd (EConstr.of_constr c))))
nc
~init:Evar.Set.empty
let undefined_evars_of_evar_info evd evi =
- Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
+ Evar.Set.union (undefined_evars_of_term evd (EConstr.of_constr evi.evar_concl))
(Evar.Set.union
(match evi.evar_body with
| Evar_empty -> Evar.Set.empty
- | Evar_defined b -> undefined_evars_of_term evd b)
+ | Evar_defined b -> undefined_evars_of_term evd (EConstr.of_constr b))
(undefined_evars_of_named_context evd
(named_context_of_val evi.evar_hyps)))
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 6620bbaed..82346b24e 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -121,7 +121,7 @@ val advance : evar_map -> evar -> evar option
This is roughly a combination of the previous functions and
[nf_evar]. *)
-val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
+val undefined_evars_of_term : evar_map -> EConstr.constr -> Evar.Set.t
val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
diff --git a/engine/termops.ml b/engine/termops.ml
index b7932665a..c2d862f00 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1074,7 +1074,7 @@ let global_vars_set env sigma constr =
let rec filtrec acc c =
let acc = match EConstr.kind sigma c with
| Var _ | Const _ | Ind _ | Construct _ ->
- Id.Set.union (vars_of_global env (EConstr.Unsafe.to_constr c)) acc
+ Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) acc
| _ -> acc
in
EConstr.fold sigma filtrec acc c
diff --git a/engine/termops.mli b/engine/termops.mli
index 7758a57ee..013efcbcb 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -256,6 +256,7 @@ val compact_named_context : Context.Named.t -> Context.Compacted.t
val clear_named_body : Id.t -> env -> env
val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list
+val global_vars_set : env -> Evd.evar_map -> EConstr.t -> Id.Set.t
val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t
val global_app_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses * EConstr.constr option
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index faf545d4f..bcfa13c79 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -47,16 +47,16 @@ let with_delayed_uconstr ist c tac =
let replace_in_clause_maybe_by ist c1 c2 cl tac =
with_delayed_uconstr ist c1
- (fun c1 -> replace_in_clause_maybe_by c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))
+ (fun c1 -> replace_in_clause_maybe_by (EConstr.of_constr c1) c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))
let replace_term ist dir_opt c cl =
- with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
+ with_delayed_uconstr ist c (fun c -> replace_term dir_opt (EConstr.of_constr c) cl)
let clause = Pltac.clause_dft_concl
TACTIC EXTEND replace
["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
--> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
+-> [ replace_in_clause_maybe_by ist c1 (EConstr.of_constr c2) cl tac ]
END
TACTIC EXTEND replace_term_left
@@ -153,9 +153,9 @@ let injHyp id =
injection_main false { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma }
TACTIC EXTEND dependent_rewrite
-| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
+| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b (EConstr.of_constr c) ]
| [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ]
- -> [ rewriteInHyp b c id ]
+ -> [ rewriteInHyp b (EConstr.of_constr c) id ]
END
(** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to
@@ -163,9 +163,9 @@ END
"cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *)
TACTIC EXTEND cut_rewrite
-| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
+| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b (EConstr.of_constr eqn) ]
| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
- -> [ cutRewriteInHyp b eqn id ]
+ -> [ cutRewriteInHyp b (EConstr.of_constr eqn) id ]
END
(**********************************************************************)
@@ -235,7 +235,7 @@ END
let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) =
let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in
with_delayed_uconstr ist c
- (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true)
+ (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (EConstr.of_constr c,NoBindings) true)
TACTIC EXTEND rewrite_star
| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
@@ -719,7 +719,7 @@ let rewrite_except h =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let hyps = Tacmach.New.pf_ids_of_hyps gl in
Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else
- Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
+ Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (EConstr.mkVar h) false))
hyps
end }
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index ef2ab0917..0d279ae93 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -2094,6 +2094,7 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
(** Setoid rewriting when called with "rewrite" *)
let general_s_rewrite cl l2r occs (c,l) ~new_goals =
Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let (c,l) = Miscops.map_with_bindings EConstr.Unsafe.to_constr (c,l) in
let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
let unify env evars t = unify_abs res l2r sort env evars t in
let app = apply_rule unify occs in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7b023413d..a12ef00ec 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -229,7 +229,8 @@ let make_prb gls depth additionnal_terms =
let build_projection intype (cstr:pconstructor) special default gls=
let ci= (snd(fst cstr)) in
- let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+ let body=Equality.build_selector (pf_env gls) (project gls) ci (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) (EConstr.of_constr default) in
+ let body = EConstr.Unsafe.to_constr body in
let id=pf_get_new_id (Id.of_string "t") gls in
mkLambda(Name id,intype,body)
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index fa64b276c..dbb5cc2de 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -600,15 +600,15 @@ let rec fourier () =
(Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
else get coq_Rnot_le_le))
(Tacticals.New.tclTHENS (Equality.replace
- (mkAppL [|cget coq_Rminus;!t2;!t1|]
- )
- tc)
+ (EConstr.of_constr (mkAppL [|cget coq_Rminus;!t2;!t1|]
+ ))
+ (EConstr.of_constr tc))
[tac2;
(Tacticals.New.tclTHENS
(Equality.replace
- (mkApp (cget coq_Rinv,
- [|cget coq_R1|]))
- (cget coq_R1))
+ (EConstr.of_constr (mkApp (cget coq_Rinv,
+ [|cget coq_R1|])))
+ (get coq_R1))
(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
[Tacticals.New.tclORELSE
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 940f1669a..2e3992be9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -401,7 +401,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
| [] -> anomaly (Pp.str "Cannot find a way to prove recursive property");
| eq_id::eq_ids ->
tclTHEN
- (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id))))
+ (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar eq_id))))
(do_rewrite eq_ids)
g
in
@@ -1060,7 +1060,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
let just_introduced = nLastDecls nb_intro_to_do g' in
let open Context.Named.Declaration in
let just_introduced_id = List.map get_id just_introduced in
- tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma))
+ tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr equation_lemma)))
(revert just_introduced_id) g'
)
g
@@ -1425,7 +1425,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
let backtrack_eqs_until_hrec hrec eqs : tactic =
fun gls ->
- let eqs = List.map mkVar eqs in
+ let eqs = List.map EConstr.mkVar eqs in
let rewrite =
tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
in
@@ -1453,7 +1453,7 @@ let rec rewrite_eqs_in_eqs eqs =
observe_tac
(Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id))
(tclTRY (Proofview.V82.of_tactic (Equality.general_rewrite_in true Locus.AllOccurrences
- true (* dep proofs also: *) true id (mkVar eq) false)))
+ true (* dep proofs also: *) true id (EConstr.mkVar eq) false)))
gl
)
eqs
@@ -1659,7 +1659,7 @@ let prove_principle_for_gen
(* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1)));
(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *)
h_intros (List.rev (acc_rec_arg_id::args_ids));
- Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
+ Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_ref)));
(* observe_tac "finish" *) (fun gl' ->
let body =
let _,args = destApp (pf_concl gl') in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a45effb16..08b40a1f7 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -502,6 +502,7 @@ let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (G
| _ -> assert false;;
let list_rewrite (rev:bool) (eqs: (constr*bool) list) =
+ let eqs = List.map (Util.on_fst EConstr.of_constr) eqs in
tclREPEAT
(List.fold_right
(fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 36fb6dad3..d29d4694f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -385,7 +385,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
(* introducing the the result of the graph and the equality hypothesis *)
observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
(* replacing [res] with its value *)
- observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
+ observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar hres)));
(* Conclusion *)
observe_tac "exact" (fun g ->
Proofview.V82.of_tactic (exact_check (EConstr.of_constr (app_constructor g))) g)
@@ -520,7 +520,7 @@ and intros_with_rewrite_aux : tactic =
let id = pf_get_new_id (Id.of_string "y") g in
tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
generalize_dependent_of (destVar args.(1)) id;
- tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
+ tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id)));
intros_with_rewrite
]
g
@@ -529,7 +529,7 @@ and intros_with_rewrite_aux : tactic =
let id = pf_get_new_id (Id.of_string "y") g in
tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
generalize_dependent_of (destVar args.(2)) id;
- tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
+ tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar id)));
intros_with_rewrite
]
g
@@ -538,7 +538,7 @@ and intros_with_rewrite_aux : tactic =
let id = pf_get_new_id (Id.of_string "y") g in
tclTHENSEQ[
Proofview.V82.of_tactic (Simple.intro id);
- tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
+ tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id)));
intros_with_rewrite
] g
end
@@ -709,7 +709,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
in
tclTHENSEQ[
tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids;
- Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
+ Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_lemma)));
(* Don't forget to $\zeta$ normlize the term since the principles
have been $\zeta$-normalized *)
Proofview.V82.of_tactic (reduce
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 74affa396..5cee3cb20 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -871,10 +871,10 @@ let rec make_rewrite_list expr_info max = function
in
Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
true (* dep proofs also: *) true
- (mkVar hp,
+ (EConstr.mkVar hp,
ExplicitBindings[Loc.ghost,NamedHyp def,
- expr_info.f_constr;Loc.ghost,NamedHyp k,
- (f_S max)]) false) g) )
+ EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k,
+ EConstr.of_constr (f_S max)]) false) g) )
)
[make_rewrite_list expr_info max l;
observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *)
@@ -898,10 +898,10 @@ let make_rewrite expr_info l hp max =
observe_tac (str "general_rewrite_bindings")
(Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
true (* dep proofs also: *) true
- (mkVar hp,
+ (EConstr.mkVar hp,
ExplicitBindings[Loc.ghost,NamedHyp def,
- expr_info.f_constr;Loc.ghost,NamedHyp k,
- (f_S (f_S max))]) false)) g)
+ EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k,
+ EConstr.of_constr (f_S (f_S max))]) false)) g)
[observe_tac(str "make_rewrite finalize") (
(* tclORELSE( h_reflexivity) *)
(observe_tclTHENLIST (str "make_rewrite")[
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index b567344c9..d656206d6 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -122,7 +122,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
Tacticals.New.tclTHEN tac
(one_base (fun dir c tac ->
let tac = (tac, conds) in
- general_rewrite dir AllOccurrences true false ~tac c)
+ general_rewrite dir AllOccurrences true false ~tac (EConstr.of_constr c))
tac_main bas))
(Proofview.tclUNIT()) lbas))
@@ -165,7 +165,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
| _ -> assert false) (* there must be at least an hypothesis *)
| _ -> assert false (* rewriting cannot complete a proof *)
in
- let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y z w) in
+ let general_rewrite_in x y z w = Proofview.V82.tactic (general_rewrite_in x y (EConstr.of_constr z) w) in
Tacticals.New.tclMAP (fun id ->
Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS
(List.fold_left (fun tac bas ->
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7d8fc79f4..02211efd6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1315,8 +1315,8 @@ module Intpart = Unionfind.Make(Evar.Set)(Evar.Map)
let deps_of_constraints cstrs evm p =
List.iter (fun (_, _, x, y) ->
- let evx = Evarutil.undefined_evars_of_term evm x in
- let evy = Evarutil.undefined_evars_of_term evm y in
+ let evx = Evarutil.undefined_evars_of_term evm (EConstr.of_constr x) in
+ let evy = Evarutil.undefined_evars_of_term evm (EConstr.of_constr y) in
Intpart.union_set (Evar.Set.union evx evy) p)
cstrs
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index eb75cbf7d..be9a34239 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -116,7 +116,7 @@ let rec rewrite_and_clear hyps = match hyps with
| [] -> Proofview.tclUNIT ()
| id :: hyps ->
tclTHENLIST [
- Equality.rewriteLR (mkVar id);
+ Equality.rewriteLR (EConstr.mkVar id);
clear [id];
rewrite_and_clear hyps;
]
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 80f83f19b..4c79a6199 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -12,8 +12,9 @@ open Util
open Names
open Nameops
open Term
-open Vars
open Termops
+open EConstr
+open Vars
open Namegen
open Inductive
open Inductiveops
@@ -46,6 +47,10 @@ 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)
+
(* Options *)
let discriminate_introduction = ref true
@@ -144,7 +149,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 (EConstr.Unsafe.to_constr (clenv_type clause)) in
+ let newevars = Evarutil.undefined_evars_of_term sigma (clenv_type clause) in
let evars =
fold_undefined (fun evk _ evars ->
if Evar.Set.mem evk newevars then evars
@@ -165,11 +170,9 @@ 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 sigma = project gl in
let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
- let (equiv, args) = decompose_appvect (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
+ let (equiv, args) = decompose_app_vect sigma (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
@@ -184,11 +187,9 @@ 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 c = EConstr.of_constr c in
let sigma, ct = pf_type_of gl c in
let ct = EConstr.of_constr ct in
let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct 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]
@@ -332,9 +333,9 @@ let (forward_general_setoid_rewrite_clause, general_setoid_rewrite_clause) = Hoo
let jmeq_same_dom gl = function
| None -> true (* already checked in Hipattern.find_eq_data_decompose *)
| Some t ->
- let rels, t = decompose_prod_assum t in
+ let rels, t = decompose_prod_assum (project gl) t in
let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in
- match EConstr.decompose_app (project gl) (EConstr.of_constr t) with
+ match decompose_app (project gl) t with
| _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
| _ -> false
@@ -342,6 +343,8 @@ let jmeq_same_dom gl = function
eliminate lbeq on sort_of_gl. *)
let find_elim hdcncl lft2rgt dep cls ot gl =
+ let sigma = project gl in
+ let is_global gr c = Termops.is_global sigma gr c in
let inccl = Option.is_empty cls in
if (is_global Coqlib.glob_eq hdcncl ||
(is_global Coqlib.glob_jmeq hdcncl &&
@@ -349,7 +352,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
|| Flags.version_less_or_equal Flags.V8_2
then
let c =
- match kind_of_term hdcncl with
+ match EConstr.kind sigma hdcncl with
| Ind (ind_sp,u) ->
let pr1 =
lookup_eliminator ind_sp (elimination_sort_of_clause cls gl)
@@ -377,6 +380,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
assert false
in
let Sigma (elim, sigma, p) = Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+ let elim = EConstr.of_constr elim in
Sigma ((elim, Safe_typing.empty_private_constants), sigma, p)
else
let scheme_name = match dep, lft2rgt, inccl with
@@ -391,13 +395,14 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
| true, _, true -> rew_r2l_dep_scheme_kind
| true, _, false -> rew_r2l_forward_dep_scheme_kind
in
- match kind_of_term hdcncl with
+ match EConstr.kind sigma hdcncl with
| Ind (ind,u) ->
let c, eff = find_scheme scheme_name ind in
(* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
let Sigma (elim, sigma, p) =
Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
in
+ let elim = EConstr.of_constr elim in
Sigma ((elim, eff), sigma, p)
| _ -> assert false
@@ -408,12 +413,12 @@ let type_of_clause cls gl = match cls with
let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
- let isatomic = isProd (whd_zeta evd (EConstr.of_constr hdcncl)) in
+ let isatomic = isProd evd (EConstr.of_constr (whd_zeta evd hdcncl)) in
let dep_fun = if isatomic then dependent else dependent_no_evar in
let type_of_cls = type_of_clause cls gl in
- let dep = dep_proof_ok && dep_fun evd (EConstr.of_constr c) (EConstr.of_constr type_of_cls) in
+ let type_of_cls = EConstr.of_constr type_of_cls in
+ let dep = dep_proof_ok && dep_fun evd c type_of_cls in
let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
- let elim = EConstr.of_constr elim in
let tac =
Proofview.tclEFFECTS effs <*>
general_elim_clause with_evars frzevars tac cls c t l
@@ -447,11 +452,11 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
- let ctype = get_type_of env sigma (EConstr.of_constr c) in
- let rels, t = decompose_prod_assum (whd_betaiotazeta sigma (EConstr.of_constr ctype)) in
- match match_with_equality_type sigma (EConstr.of_constr t) with
+ let ctype = get_type_of env sigma c in
+ let ctype = EConstr.of_constr ctype in
+ let rels, t = decompose_prod_assum sigma (EConstr.of_constr (whd_betaiotazeta sigma ctype)) in
+ match match_with_equality_type sigma t with
| Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
- let hdcncl = EConstr.Unsafe.to_constr hdcncl in
let lft2rgt = adjust_rewriting_direction args lft2rgt in
leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels)
l with_evars frzevars dep_proof_ok hdcncl
@@ -465,10 +470,10 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
| (e, info) ->
Proofview.tclEVARMAP >>= fun sigma ->
let env' = push_rel_context rels env in
- let rels',t' = splay_prod_assum env' sigma (EConstr.of_constr t) in (* Search for underlying eq *)
- match match_with_equality_type sigma (EConstr.of_constr t') with
+ let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
+ let t' = EConstr.of_constr t' in
+ match match_with_equality_type sigma t' with
| Some (hdcncl,args) ->
- let hdcncl = EConstr.Unsafe.to_constr hdcncl in
let lft2rgt = adjust_rewriting_direction args lft2rgt in
leibniz_rewrite_ebindings_clause cls lft2rgt tac c
(it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl
@@ -533,7 +538,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
let do_hyps =
(* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
let ids gl =
- let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
+ let ids_in_c = Termops.global_vars_set (Global.env()) (project gl) (fst c) in
let ids_of_hyps = pf_ids_of_hyps gl in
Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
in
@@ -563,7 +568,6 @@ let general_multi_rewrite with_evars l cl tac =
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let (c, sigma) = run_delayed env sigma f in
- let c = Miscops.map_with_bindings EConstr.Unsafe.to_constr c in
tclWITHHOLES with_evars
(general_rewrite_clause l2r with_evars ?tac c cl) sigma
end }
@@ -631,12 +635,14 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
in
Proofview.Goal.enter { enter = begin fun gl ->
let get_type_of = pf_apply get_type_of gl in
- let t1 = get_type_of (EConstr.of_constr c1)
- and t2 = get_type_of (EConstr.of_constr c2) in
+ let t1 = get_type_of c1
+ and t2 = get_type_of c2 in
+ let t1 = EConstr.of_constr t1 in
+ let t2 = EConstr.of_constr t2 in
let evd =
if unsafe then Some (Tacmach.New.project gl)
else
- try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) (EConstr.of_constr t1) (EConstr.of_constr t2) (Tacmach.New.project gl))
+ try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl))
with Evarconv.UnableToUnify _ -> None
in
match evd with
@@ -647,9 +653,9 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
let sym = build_coq_eq_sym () in
Tacticals.New.pf_constr_of_global sym (fun sym ->
Tacticals.New.pf_constr_of_global e (fun e ->
+ let e = EConstr.of_constr e in
let eq = applist (e, [t1;c1;c2]) in
let sym = EConstr.of_constr sym in
- let eq = EConstr.of_constr eq in
tclTHENLAST
(replace_core clause l2r eq)
(tclFIRST
@@ -727,12 +733,10 @@ let _ =
optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
let find_positions env sigma t1 t2 =
- let open EConstr in
let project env sorts posn t1 t2 =
- let t1 = EConstr.Unsafe.to_constr t1 in
- let t2 = EConstr.Unsafe.to_constr t2 in
- let ty1 = get_type_of env sigma (EConstr.of_constr t1) in
- let s = get_sort_family_of env sigma (EConstr.of_constr ty1) in
+ let ty1 = get_type_of env sigma t1 in
+ let ty1 = EConstr.of_constr ty1 in
+ let s = get_sort_family_of env sigma ty1 in
if Sorts.List.mem s sorts
then [(List.rev posn,t1,t2)] else []
in
@@ -854,7 +858,7 @@ let injectable env sigma t1 t2 =
let descend_then env sigma head dirn =
let IndType (indf,_) =
- try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma (EConstr.of_constr head)))
+ try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma head))
with Not_found ->
error "Cannot project on an inductive type derived from a dependency." in
let indp,_ = (dest_ind_family indf) in
@@ -871,12 +875,12 @@ let descend_then env sigma head dirn =
it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
let build_branch i =
let result = if Int.equal i dirn then dirnval else dfltval in
- it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in
+ it_mkLambda_or_LetIn result (name_context env cstr.(i-1).cs_args) in
let brl =
List.map build_branch
(List.interval 1 (Array.length mip.mind_consnames)) in
let ci = make_case_info env ind RegularStyle in
- EConstr.Unsafe.to_constr (Inductiveops.make_case_or_project env sigma indf ci (EConstr.of_constr p) (EConstr.of_constr head) (Array.map_of_list EConstr.of_constr brl))))
+ Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
(* Now we need to construct the discriminator, given a discriminable
position. This boils down to:
@@ -897,7 +901,7 @@ let descend_then env sigma head dirn =
let build_selector env sigma dirn c ind special default =
let IndType(indf,_) =
- try find_rectype env sigma (EConstr.of_constr ind)
+ try find_rectype env sigma ind
with Not_found ->
(* one can find Rel(k) in case of dependent constructors
like T := c : (A:Set)A->T and a discrimination
@@ -909,7 +913,8 @@ let build_selector env sigma dirn c ind special default =
dependent types.") in
let (indp,_) = dest_ind_family indf in
let ind, _ = check_privacy env indp in
- let typ = Retyping.get_type_of env sigma (EConstr.of_constr default) in
+ let typ = Retyping.get_type_of env sigma default in
+ let typ = EConstr.of_constr typ in
let (mib,mip) = lookup_mind_specif env ind in
let deparsign = make_arity_signature env true indf in
let p = it_mkLambda_or_LetIn typ deparsign in
@@ -922,9 +927,14 @@ let build_selector env sigma dirn c ind special default =
let ci = make_case_info env ind RegularStyle in
mkCase (ci, p, c, Array.of_list brl)
+let build_coq_False () = EConstr.of_constr (build_coq_False ())
+let build_coq_True () = EConstr.of_constr (build_coq_True ())
+let build_coq_I () = EConstr.of_constr (build_coq_I ())
+
let rec build_discriminator env sigma dirn c = function
| [] ->
- let ind = get_type_of env sigma (EConstr.of_constr c) in
+ let ind = get_type_of env sigma c in
+ let ind = EConstr.of_constr ind in
let true_0,false_0 =
build_coq_True(),build_coq_False() in
build_selector env sigma dirn c ind true_0 false_0
@@ -952,7 +962,7 @@ let gen_absurdity id =
let hyp_typ = EConstr.of_constr hyp_typ in
if is_empty_type sigma hyp_typ
then
- simplest_elim (EConstr.mkVar id)
+ simplest_elim (mkVar id)
else
tclZEROMSG (str "Not the negation of an equality.")
end }
@@ -980,6 +990,7 @@ let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq =
let absurd_term = build_coq_False () in
let eq_elim, eff = ind_scheme_of_eq lbeq in
let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in
+ let eq_elim = EConstr.of_constr eq_elim in
sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
eff
@@ -987,8 +998,6 @@ 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 EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
@@ -997,19 +1006,14 @@ let apply_on_clause (f,t) clause =
clenv_fchain ~with_univs:false argmv f_clause clause
let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
- let t = EConstr.Unsafe.to_constr t in
- let t1 = EConstr.Unsafe.to_constr t1 in
- let t2 = EConstr.Unsafe.to_constr t2 in
- let eqn = EConstr.Unsafe.to_constr eqn in
let e = next_ident_away eq_baseid (ids_of_context env) in
- let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in
+ let e_env = push_named (nlocal_assum (e, t)) env in
let discriminator =
build_discriminator e_env sigma dirn (mkVar e) cpath in
let sigma,(pf, absurd_term), eff =
discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in
let pf_ty = mkArrow eqn absurd_term in
let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
- let absurd_term = EConstr.of_constr absurd_term in
let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
Proofview.Unsafe.tclEVARS sigma <*>
Proofview.tclEFFECTS eff <*>
@@ -1047,19 +1051,20 @@ let onNegatedEquality with_evars tac =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
let ccl = Proofview.Goal.concl gl in
+ let ccl = EConstr.of_constr ccl in
let env = Proofview.Goal.env gl in
- match kind_of_term (hnf_constr env sigma (EConstr.of_constr ccl)) with
- | Prod (_,t,u) when is_empty_type sigma (EConstr.of_constr u) ->
+ match EConstr.kind sigma (EConstr.of_constr (hnf_constr env sigma ccl)) with
+ | Prod (_,t,u) when is_empty_type sigma u ->
tclTHEN introf
(onLastHypId (fun id ->
- onEquality with_evars tac (EConstr.mkVar id,NoBindings)))
+ onEquality with_evars tac (mkVar id,NoBindings)))
| _ ->
tclZEROMSG (str "Not a negated primitive equality.")
end }
let discrSimpleClause with_evars = function
| None -> onNegatedEquality with_evars discrEq
- | Some id -> onEquality with_evars discrEq (EConstr.mkVar id,NoBindings)
+ | Some id -> onEquality with_evars discrEq (mkVar id,NoBindings)
let discr with_evars = onEquality with_evars discrEq
@@ -1073,7 +1078,7 @@ let discrEverywhere with_evars =
(tclTHEN
(tclREPEAT introf)
(tryAllHyps
- (fun id -> tclCOMPLETE (discr with_evars (EConstr.mkVar id,NoBindings)))))
+ (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
else (* <= 8.2 compat *)
tryAllHypsAndConcl (discrSimpleClause with_evars))
(* (fun gls ->
@@ -1103,9 +1108,10 @@ let find_sigma_data env s = build_sigma_type ()
*)
let make_tuple env sigma (rterm,rty) lind =
- assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty)));
- let sigdata = find_sigma_data env (get_sort_of env sigma (EConstr.of_constr rty)) in
- let sigma, a = type_of ~refresh:true env sigma (EConstr.mkRel lind) in
+ assert (not (noccurn sigma lind rty));
+ let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
+ let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
+ let a = EConstr.of_constr a in
let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in
(* We move [lind] to [1] and lift other rels > [lind] by 1 *)
let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1113,6 +1119,8 @@ let make_tuple env sigma (rterm,rty) lind =
let p = mkLambda (na, a, rty) in
let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
let sigma, sig_term = Evd.fresh_global env sigma sigdata.typ in
+ let exist_term = EConstr.of_constr exist_term in
+ let sig_term = EConstr.of_constr sig_term in
sigma,
(applist(exist_term,[a;p;(mkRel lind);rterm]),
applist(sig_term,[a;p]))
@@ -1125,9 +1133,10 @@ let make_tuple env sigma (rterm,rty) lind =
normalization *)
let minimal_free_rels env sigma (c,cty) =
- let cty_rels = free_rels sigma (EConstr.of_constr cty) in
- let cty' = simpl env sigma (EConstr.of_constr cty) in
- let rels' = free_rels sigma (EConstr.of_constr cty') in
+ let cty_rels = free_rels sigma cty in
+ let cty' = simpl env sigma cty in
+ let cty' = EConstr.of_constr cty' in
+ let rels' = free_rels sigma cty' in
if Int.Set.subset cty_rels rels' then
(cty,cty_rels)
else
@@ -1139,7 +1148,7 @@ let minimal_free_rels_rec env sigma =
let rec minimalrec_free_rels_rec prev_rels (c,cty) =
let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
let combined_rels = Int.Set.union prev_rels direct_rels in
- let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (EConstr.mkRel i)))
+ let folder rels i = snd (minimalrec_free_rels_rec rels (c, EConstr.of_constr (unsafe_type_of env sigma (mkRel i))))
in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
in minimalrec_free_rels_rec Int.Set.empty
@@ -1185,27 +1194,30 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let rec sigrec_clausal_form siglen p_i =
if Int.equal siglen 0 then
(* is the default value typable with the expected type *)
- let dflt_typ = unsafe_type_of env sigma (EConstr.of_constr dflt) in
+ let dflt_typ = unsafe_type_of env sigma dflt in
try
- let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) (EConstr.of_constr p_i) !evdref in
+ let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) p_i !evdref in
let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
dflt
with Evarconv.UnableToUnify _ ->
error "Cannot solve a unification problem."
else
- let (a,p_i_minus_1) = match whd_beta_stack !evdref (EConstr.of_constr p_i) with
- | (_sigS,[a;p]) -> (EConstr.Unsafe.to_constr a, EConstr.Unsafe.to_constr p)
+ let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
+ | (_sigS,[a;p]) -> (a, p)
| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in
- let ev = Evarutil.e_new_evar env evdref (EConstr.of_constr a) in
- let rty = beta_applist sigma (EConstr.of_constr p_i_minus_1,[ev]) in
+ let ev = Evarutil.e_new_evar env evdref a in
+ let rty = beta_applist sigma (p_i_minus_1,[ev]) in
+ let rty = EConstr.of_constr rty in
let tuple_tail = sigrec_clausal_form (siglen-1) rty in
let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in
match evopt with
| Some w ->
let w_type = unsafe_type_of env !evdref w in
- if Evarconv.e_cumul env evdref (EConstr.of_constr w_type) (EConstr.of_constr a) then
+ let w_type = EConstr.of_constr w_type in
+ if Evarconv.e_cumul env evdref w_type a then
let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
- applist(exist_term,[a;p_i_minus_1;EConstr.Unsafe.to_constr w;tuple_tail])
+ let exist_term = EConstr.of_constr exist_term in
+ applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
else
error "Cannot solve a unification problem."
| None ->
@@ -1218,7 +1230,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
error "Cannot solve a unification problem."
in
let scf = sigrec_clausal_form siglen ty in
- !evdref, Evarutil.nf_evar !evdref scf
+ !evdref, EConstr.of_constr (Evarutil.nf_evar !evdref (EConstr.Unsafe.to_constr scf))
(* The problem is to build a destructor (a generalization of the
predecessor) which, when applied to a term made of constructors
@@ -1280,18 +1292,18 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let make_iterated_tuple env sigma dflt (z,zty) =
let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
- let sort_of_zty = get_sort_of env sigma (EConstr.of_constr zty) in
+ let sort_of_zty = get_sort_of env sigma zty in
let sorted_rels = Int.Set.elements rels in
let sigma, (tuple,tuplety) =
List.fold_left (fun (sigma, t) -> make_tuple env sigma t) (sigma, (z,zty)) sorted_rels
in
- assert (closed0 tuplety);
+ assert (closed0 sigma tuplety);
let n = List.length sorted_rels in
let sigma, dfltval = sig_clausal_form env sigma sort_of_zty n tuplety dflt in
sigma, (tuple,tuplety,dfltval)
let rec build_injrec env sigma dflt c = function
- | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma (EConstr.of_constr c))
+ | [] -> make_iterated_tuple env sigma dflt (c,EConstr.of_constr (unsafe_type_of env sigma c))
| ((sp,cnum),argnum)::l ->
try
let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1326,40 +1338,44 @@ let inject_if_homogenous_dependent_pair ty =
try
let sigma = Tacmach.New.project gl in
let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
- let t = EConstr.Unsafe.to_constr t in
(* fetch the informations of the pair *)
let ceq = Universes.constr_of_global Coqlib.glob_eq in
+ let ceq = EConstr.of_constr ceq in
let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in
(* check whether the equality deals with dep pairs or not *)
- let eqTypeDest = fst (decompose_app t) in
- if not (Globnames.is_global (sigTconstr()) eqTypeDest) then raise Exit;
+ let eqTypeDest = fst (decompose_app sigma t) in
+ if not (Termops.is_global sigma (sigTconstr()) eqTypeDest) then raise Exit;
let hd1,ar1 = decompose_app_vect sigma t1 and
hd2,ar2 = decompose_app_vect sigma t2 in
- if not (Globnames.is_global (existTconstr()) hd1) then raise Exit;
- if not (Globnames.is_global (existTconstr()) hd2) then raise Exit;
- let ind,_ = try pf_apply find_mrectype gl (EConstr.of_constr ar1.(0)) with Not_found -> raise Exit in
+ let hd1 = EConstr.of_constr hd1 in
+ let hd2 = EConstr.of_constr hd2 in
+ let ar1 = Array.map EConstr.of_constr ar1 in
+ let ar2 = Array.map EConstr.of_constr ar2 in
+ if not (Termops.is_global sigma (existTconstr()) hd1) then raise Exit;
+ if not (Termops.is_global sigma (existTconstr()) hd2) then raise Exit;
+ let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
(* check if the user has declared the dec principle *)
(* and compare the fst arguments of the dep pair *)
(* Note: should work even if not an inductive type, but the table only *)
(* knows inductive types *)
if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
- pf_apply is_conv gl (EConstr.of_constr ar1.(2)) (EConstr.of_constr ar2.(2))) then raise Exit;
+ pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
- let new_eq_args = [|pf_unsafe_type_of gl (EConstr.of_constr ar1.(3));ar1.(3);ar2.(3)|] in
+ let new_eq_args = [|EConstr.of_constr (pf_unsafe_type_of gl ar1.(3));ar1.(3);ar2.(3)|] in
let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
+ let inj2 = EConstr.of_constr inj2 in
let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
(* cut with the good equality and prove the requested goal *)
tclTHENLIST
[Proofview.tclEFFECTS eff;
intro;
onLastHyp (fun hyp ->
- let hyp = EConstr.Unsafe.to_constr hyp in
- tclTHENS (cut (EConstr.of_constr (mkApp (ceq,new_eq_args))))
- [clear [destVar hyp];
+ tclTHENS (cut (mkApp (ceq,new_eq_args)))
+ [clear [destVar sigma hyp];
Proofview.V82.tactic (Tacmach.refine
- (EConstr.of_constr (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
+ (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
])]
with Exit ->
Proofview.tclUNIT ()
@@ -1371,17 +1387,15 @@ let inject_if_homogenous_dependent_pair ty =
let simplify_args env sigma t =
(* Quick hack to reduce in arguments of eq only *)
- match decompose_app t with
- | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma (EConstr.of_constr c1);simpl env sigma (EConstr.of_constr c2)])
- | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma (EConstr.of_constr c1);t2;simpl env sigma (EConstr.of_constr c2)])
+ let simpl env sigma c = EConstr.of_constr (simpl env sigma c) in
+ match decompose_app sigma t with
+ | eq, [t;c1;c2] -> applist (eq,[t;simpl env sigma c1;simpl env sigma c2])
+ | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2])
| _ -> t
let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
- let t = EConstr.Unsafe.to_constr t in
- let t1 = EConstr.Unsafe.to_constr t1 in
- let t2 = EConstr.Unsafe.to_constr t2 in
let e = next_ident_away eq_baseid (ids_of_context env) in
- let e_env = push_named (LocalAssum (e,t)) env in
+ let e_env = push_named (nlocal_assum (e,t)) env in
let evdref = ref sigma in
let filter (cpath, t1', t2') =
try
@@ -1389,12 +1403,13 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in
let injfun = mkNamedLambda e t injbody in
let sigma,congr = Evd.fresh_global env sigma eq.congr in
+ let congr = EConstr.of_constr congr in
let pf = applist(congr,[t;resty;injfun;t1;t2]) in
- let sigma, pf_typ = Typing.type_of env sigma (EConstr.of_constr pf) in
+ let sigma, pf_typ = Typing.type_of env sigma pf in
+ let pf_typ = EConstr.of_constr pf_typ 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 (EConstr.Unsafe.to_constr (clenv_type inj_clause)) in
- let pf = EConstr.Unsafe.to_constr pf in
+ let ty = simplify_args env sigma (clenv_type inj_clause) in
evdref := sigma;
Some (pf, ty)
with Failure _ -> None
@@ -1406,9 +1421,9 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
(Tacticals.New.tclTHENFIRST
(Proofview.tclIGNORE (Proofview.Monad.List.map
- (fun (pf,ty) -> tclTHENS (cut (EConstr.of_constr ty))
- [inject_if_homogenous_dependent_pair (EConstr.of_constr ty);
- Proofview.V82.tactic (Tacmach.refine (EConstr.of_constr pf))])
+ (fun (pf,ty) -> tclTHENS (cut ty)
+ [inject_if_homogenous_dependent_pair ty;
+ Proofview.V82.tactic (Tacmach.refine pf)])
(if l2r then List.rev injectors else injectors)))
(tac (List.length injectors)))
@@ -1428,7 +1443,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 (EConstr.Unsafe.to_constr (clenv_value eq_clause)))
+ (tac (clenv_value eq_clause))
let get_previous_hyp_position id gl =
let rec aux dest = function
@@ -1451,10 +1466,10 @@ let injEq ?(old=false) with_evars clear_flag ipats =
match ipats_style with
| Some ipats ->
Proofview.Goal.enter { enter = begin fun gl ->
- let destopt = match kind_of_term c with
+ let sigma = project gl in
+ let destopt = match EConstr.kind sigma c with
| Var id -> get_previous_hyp_position id gl
| _ -> MoveLast in
- let c = EConstr.of_constr c in
let clear_tac =
tclTRY (apply_clear_request clear_flag dft_clear_flag c) in
(* Try should be removal if dependency were treated *)
@@ -1488,10 +1503,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 (EConstr.Unsafe.to_constr (clenv_value clause)) 0
+ ntac (clenv_value clause) 0
| Inr posns ->
inject_at_positions env sigma true u clause posns
- (ntac (EConstr.Unsafe.to_constr (clenv_value clause)))
+ (ntac (clenv_value clause))
end }
let dEqThen with_evars ntac = function
@@ -1500,7 +1515,6 @@ let dEqThen with_evars ntac = function
let dEq with_evars =
dEqThen with_evars (fun clear_flag c x ->
- let c = EConstr.of_constr c in
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
let intro_decomp_eq tac data (c, t) =
@@ -1547,26 +1561,24 @@ let decomp_tuple_term env sigma c t =
let rec decomprec inner_code ex exty =
let iterated_decomp =
try
- let ex = EConstr.of_constr ex in
let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose sigma ex in
- let a = EConstr.Unsafe.to_constr a in
- let p = EConstr.Unsafe.to_constr p in
- let car = EConstr.Unsafe.to_constr car in
- let cdr = EConstr.Unsafe.to_constr cdr in
let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code])
and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in
- let cdrtyp = beta_applist sigma (EConstr.of_constr p,[EConstr.of_constr car]) in
+ let cdrtyp = beta_applist sigma (p,[car]) in
+ let cdrtyp = EConstr.of_constr cdrtyp in
List.map (fun l -> ((car,a),car_code)::l) (decomprec cdr_code cdr cdrtyp)
with Constr_matching.PatternMatchingFailure ->
[]
in [((ex,exty),inner_code)]::iterated_decomp
in decomprec (mkRel 1) c t
+let lambda_create env (a,b) =
+ mkLambda (named_hd env (EConstr.Unsafe.to_constr a) Anonymous, a, b)
+
let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
- let dep_pair1 = EConstr.Unsafe.to_constr dep_pair1 in
- let dep_pair2 = EConstr.Unsafe.to_constr dep_pair2 in
let sigma = Sigma.to_evar_map sigma in
- let typ = get_type_of env sigma (EConstr.of_constr dep_pair1) in
+ let typ = get_type_of env sigma dep_pair1 in
+ let typ = EConstr.of_constr typ in
(* We find all possible decompositions *)
let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in
let decomps2 = decomp_tuple_term env sigma dep_pair2 typ in
@@ -1581,15 +1593,18 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
(* We build the expected goal *)
let abst_B =
List.fold_right
- (fun (e,t) body -> lambda_create env (t,subst_term sigma (EConstr.of_constr e) (EConstr.of_constr body))) e1_list b in
- let pred_body = beta_applist sigma (EConstr.of_constr abst_B, List.map EConstr.of_constr proj_list) in
+ (fun (e,t) body -> lambda_create env (t,EConstr.of_constr (subst_term sigma e body))) e1_list b in
+ let pred_body = beta_applist sigma (abst_B,proj_list) in
+ let pred_body = EConstr.of_constr pred_body in
let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in
- let expected_goal = beta_applist sigma (EConstr.of_constr abst_B,List.map (fst %> EConstr.of_constr) e2_list) in
+ let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in
(* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
- let expected_goal = nf_betaiota sigma (EConstr.of_constr expected_goal) in
+ let expected_goal = EConstr.of_constr expected_goal in
+ let expected_goal = nf_betaiota sigma expected_goal in
+ let expected_goal = EConstr.of_constr expected_goal in
(* Retype to get universes right *)
- let sigma, expected_goal_ty = Typing.type_of env sigma (EConstr.of_constr expected_goal) in
- let sigma, _ = Typing.type_of env sigma (EConstr.of_constr body) in
+ let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
+ let sigma, _ = Typing.type_of env sigma body in
Sigma.Unsafe.of_pair ((body, expected_goal), sigma)
(* Like "replace" but decompose dependent equalities *)
@@ -1598,16 +1613,14 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
(* on for further iterated sigma-tuples *)
let cutSubstInConcl l2r eqn =
- let eqn = EConstr.of_constr eqn in
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
let typ = pf_concl gl in
+ let typ = EConstr.of_constr typ in
let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
- let typ = EConstr.of_constr typ in
- let expected = EConstr.of_constr expected in
let tac =
tclTHENFIRST
(tclTHENLIST [
@@ -1620,16 +1633,14 @@ let cutSubstInConcl l2r eqn =
end }
let cutSubstInHyp l2r eqn id =
- let eqn = EConstr.of_constr eqn in
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
let typ = pf_get_hyp_typ id gl in
+ let typ = EConstr.of_constr typ in
let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in
- let typ = EConstr.of_constr typ in
- let expected = EConstr.of_constr expected in
let tac =
tclTHENFIRST
(tclTHENLIST [
@@ -1661,9 +1672,9 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
let substClause l2r c cls =
- let c = EConstr.of_constr c in
Proofview.Goal.enter { enter = begin fun gl ->
let eq = pf_apply get_type_of gl c in
+ let eq = EConstr.of_constr eq in
tclTHENS (cutSubstClause l2r eq cls)
[Proofview.tclUNIT (); exact_no_check c]
end }
@@ -1707,7 +1718,7 @@ let restrict_to_eq_and_identity eq = (* compatibility *)
not (is_global glob_identity eq)
then raise Constr_matching.PatternMatchingFailure
-exception FoundHyp of (Id.t * EConstr.constr * bool)
+exception FoundHyp of (Id.t * constr * bool)
(* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *)
let is_eq_x gl x d =
@@ -1779,7 +1790,7 @@ let subst_one_var dep_proof_ok x =
user_err ~hdr:"Subst"
(str "Cannot find any non-recursive equality over " ++ pr_id x ++
str".")
- with FoundHyp (id, c, b) -> (id, EConstr.Unsafe.to_constr c, b) in
+ with FoundHyp res -> res in
subst_one dep_proof_ok x res
end }
@@ -1811,15 +1822,14 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
let find_equations gl =
let gl = Proofview.Goal.assume gl in
let env = Proofview.Goal.env gl in
+ let sigma = project gl in
let find_eq_data_decompose = find_eq_data_decompose gl in
let select_equation_name decl =
try
let lbeq,u,(_,x,y) = find_eq_data_decompose (EConstr.of_constr (NamedDecl.get_type decl)) in
- let x = EConstr.Unsafe.to_constr x in
- let y = EConstr.Unsafe.to_constr y in
let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
- match kind_of_term x, kind_of_term y with
+ match EConstr.kind sigma x, EConstr.kind sigma y with
| Var z, _ when not (is_evaluable env (EvalVarRef z)) ->
Some (NamedDecl.get_id decl)
| _, Var z when not (is_evaluable env (EvalVarRef z)) ->
@@ -1842,14 +1852,12 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
let c = EConstr.of_constr c in
let _,_,(_,x,y) = find_eq_data_decompose c in
- let x = EConstr.Unsafe.to_constr x in
- let y = EConstr.Unsafe.to_constr y in
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
- if Term.eq_constr x y then Proofview.tclUNIT () else
- match kind_of_term x, kind_of_term y with
- | Var x', _ when not (occur_term sigma (EConstr.of_constr x) (EConstr.of_constr y)) && not (is_evaluable env (EvalVarRef x')) ->
+ if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
+ match EConstr.kind sigma x, EConstr.kind sigma y with
+ | Var x', _ when not (occur_term sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
- | _, Var y' when not (occur_term sigma (EConstr.of_constr y) (EConstr.of_constr x)) && not (is_evaluable env (EvalVarRef y')) ->
+ | _, Var y' when not (occur_term sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
| _ ->
Proofview.tclUNIT ()
@@ -1866,19 +1874,18 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
or situations like "a = S b, b = S a", or also accidentally unfolding
let-ins *)
Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let sigma = project gl in
let find_eq_data_decompose = find_eq_data_decompose gl in
let test (_,c) =
try
let c = EConstr.of_constr c in
let lbeq,u,(_,x,y) = find_eq_data_decompose c in
- let x = EConstr.Unsafe.to_constr x in
- let y = EConstr.Unsafe.to_constr y in
let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
if flags.only_leibniz then restrict_to_eq_and_identity eq;
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
- if Term.eq_constr x y then failwith "caught";
- match kind_of_term x with Var x -> x | _ ->
- match kind_of_term y with Var y -> y | _ -> failwith "caught"
+ if EConstr.eq_constr sigma x y then failwith "caught";
+ match EConstr.kind sigma x with Var x -> x | _ ->
+ match EConstr.kind sigma y with Var y -> y | _ -> failwith "caught"
with Constr_matching.PatternMatchingFailure -> failwith "caught" in
let test p = try Some (test p) with Failure _ -> None in
let hyps = pf_hyps_types gl in
@@ -1892,24 +1899,21 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
let cond_eq_term_left c t gl =
try
- let t = EConstr.of_constr t in
let (_,x,_) = pi3 (find_eq_data_decompose gl t) in
- if pf_conv_x gl (EConstr.of_constr c) x then true else failwith "not convertible"
+ if pf_conv_x gl c x then true else failwith "not convertible"
with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
let cond_eq_term_right c t gl =
try
- let t = EConstr.of_constr t in
let (_,_,x) = pi3 (find_eq_data_decompose gl t) in
- if pf_conv_x gl (EConstr.of_constr c) x then false else failwith "not convertible"
+ if pf_conv_x gl c x then false else failwith "not convertible"
with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
let cond_eq_term c t gl =
try
- let t = EConstr.of_constr t in
let (_,x,y) = pi3 (find_eq_data_decompose gl t) in
- if pf_conv_x gl (EConstr.of_constr c) x then true
- else if pf_conv_x gl (EConstr.of_constr c) y then false
+ if pf_conv_x gl c x then true
+ else if pf_conv_x gl c y then false
else failwith "not convertible"
with Constr_matching.PatternMatchingFailure -> failwith "not an equality"
@@ -1920,7 +1924,7 @@ let rewrite_assumption_cond cond_eq_term cl =
let id = NamedDecl.get_id hyp in
begin
try
- let dir = cond_eq_term (NamedDecl.get_type hyp) gl in
+ let dir = cond_eq_term (EConstr.of_constr (NamedDecl.get_type hyp)) gl in
general_rewrite_clause dir false (mkVar id,NoBindings) cl
with | Failure _ | UserError _ -> arec rest gl
end
@@ -1946,7 +1950,7 @@ let replace_term dir_opt c =
(* Declare rewriting tactic for intro patterns "<-" and "->" *)
let _ =
- let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars (Miscops.map_with_bindings EConstr.Unsafe.to_constr tac) c in
+ let gmr l2r with_evars tac c = general_rewrite_clause l2r with_evars tac c in
Hook.set Tactics.general_rewrite_clause gmr
let _ = Hook.set Tactics.subst_one subst_one
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 97f51ae20..5467b4af2 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -10,6 +10,7 @@
open Names
open Term
open Evd
+open EConstr
open Environ
open Ind_tables
open Locus
@@ -60,30 +61,30 @@ val general_rewrite_clause :
orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic
val general_multi_rewrite :
- evars_flag -> (bool * multi * clear_flag * EConstr.constr with_bindings delayed_open) list ->
+ evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list ->
clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.tactic option -> unit Proofview.tactic
val replace : constr -> constr -> unit Proofview.tactic
val replace_by : constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic
-val discr : evars_flag -> EConstr.constr with_bindings -> unit Proofview.tactic
+val discr : evars_flag -> constr with_bindings -> unit Proofview.tactic
val discrConcl : unit Proofview.tactic
val discrHyp : Id.t -> unit Proofview.tactic
val discrEverywhere : evars_flag -> unit Proofview.tactic
val discr_tac : evars_flag ->
- EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings destruction_arg option -> unit Proofview.tactic
val inj : intro_patterns option -> evars_flag ->
- clear_flag -> EConstr.constr with_bindings -> unit Proofview.tactic
+ clear_flag -> constr with_bindings -> unit Proofview.tactic
val injClause : intro_patterns option -> evars_flag ->
- EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings destruction_arg option -> unit Proofview.tactic
val injHyp : clear_flag -> Id.t -> unit Proofview.tactic
val injConcl : unit Proofview.tactic
val simpleInjClause : evars_flag ->
- EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic
+ constr with_bindings destruction_arg option -> unit Proofview.tactic
-val dEq : evars_flag -> EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic
-val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
val make_iterated_tuple :
env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
@@ -96,8 +97,8 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
val rewriteInConcl : bool -> constr -> unit Proofview.tactic
-val discriminable : env -> evar_map -> EConstr.constr -> EConstr.constr -> bool
-val injectable : env -> evar_map -> EConstr.constr -> EConstr.constr -> bool
+val discriminable : env -> evar_map -> constr -> constr -> bool
+val injectable : env -> evar_map -> constr -> constr -> bool
(* Subst *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 560e7e43d..c31e86383 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -737,7 +737,7 @@ let secvars_of_idset s =
else p) s Id.Pred.empty
let secvars_of_constr env c =
- secvars_of_idset (global_vars_set env c)
+ secvars_of_idset (Environ.global_vars_set env c)
let secvars_of_global env gr =
secvars_of_idset (vars_of_global_reference env gr)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index c66b356c7..ad2e2fa3b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -113,7 +113,15 @@ let make_inv_predicate env evd indf realargs id status concl =
if closed0 ti then
(xi,ti,ai)
else
+ let xi = EConstr.of_constr xi in
+ let ti = EConstr.of_constr ti in
+ let ai = EConstr.of_constr ai in
let sigma, res = make_iterated_tuple env' !evd ai (xi,ti) in
+ let (xi, ti, ai) = res in
+ let xi = EConstr.Unsafe.to_constr xi in
+ let ti = EConstr.Unsafe.to_constr ti in
+ let ai = EConstr.Unsafe.to_constr ai in
+ let res = (xi, ti, ai) in
evd := sigma; res
in
let eq_term = eqdata.Coqlib.eq in
@@ -334,7 +342,7 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
let projectAndApply as_mode thin avoid id eqname names depids =
let subst_hyp l2r id =
- tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id)))
+ tclTHEN (tclTRY(rewriteInConcl l2r (EConstr.mkVar id)))
(if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
in
let substHypIfVariable tac id =
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 7759c400c..f8ca8343c 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -338,6 +338,8 @@ so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
*)
(* used in the leib -> bool side*)
let do_replace_lb mode lb_scheme_key aavoid narg p q =
+ let p = EConstr.of_constr p in
+ let q = EConstr.of_constr q in
let avoid = Array.of_list aavoid in
let do_arg v offset =
try
@@ -363,7 +365,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
)
in
Proofview.Goal.nf_enter { enter = begin fun gl ->
- let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl (EConstr.of_constr p)) gl in
+ let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in
let u,v = destruct_ind type_of_pq
in let lb_type_of_p =
try
@@ -425,9 +427,11 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let rec aux l1 l2 =
match (l1,l2) with
| (t1::q1,t2::q2) ->
+ let t1 = EConstr.of_constr t1 in
+ let t2 = EConstr.of_constr t2 in
Proofview.Goal.enter { enter = begin fun gl ->
- let tt1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t1) in
- if Term.eq_constr t1 t2 then aux q1 q2
+ let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
+ if EConstr.eq_constr (Tacmach.New.project gl) t1 t2 then aux q1 q2
else (
let u,v = try destruct_ind tt1
(* trick so that the good sequence is returned*)
@@ -923,7 +927,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
Equality.general_rewrite_bindings_in true
Locus.AllOccurrences true false
(List.hd !avoid)
- ((mkVar (List.hd (List.tl !avoid))),
+ ((EConstr.mkVar (List.hd (List.tl !avoid))),
NoBindings
)
true;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 06:02:29 +0000