aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ltac/extratactics.ml424
-rw-r--r--ltac/g_class.ml46
-rw-r--r--ltac/rewrite.ml8
-rw-r--r--ltac/tacinterp.ml30
-rw-r--r--plugins/cc/cctac.ml44
-rw-r--r--plugins/omega/coq_omega.ml35
-rw-r--r--proofs/clenv.ml17
-rw-r--r--proofs/clenv.mli11
-rw-r--r--proofs/clenvtac.ml4
-rw-r--r--tactics/auto.ml16
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/class_tactics.ml42
-rw-r--r--tactics/class_tactics.mli2
-rw-r--r--tactics/contradiction.ml2
-rw-r--r--tactics/eauto.ml17
-rw-r--r--tactics/elim.ml4
-rw-r--r--tactics/eqdecide.ml4
-rw-r--r--tactics/equality.ml24
-rw-r--r--tactics/inv.ml14
-rw-r--r--tactics/leminv.ml5
-rw-r--r--tactics/tacticals.ml140
-rw-r--r--tactics/tacticals.mli5
-rw-r--r--tactics/tactics.ml107
-rw-r--r--tactics/tactics.mli4
-rw-r--r--toplevel/auto_ind_decl.ml32
25 files changed, 305 insertions, 294 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 58c5823c5..e9d91fe47 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -354,7 +354,7 @@ let constr_flags = {
Pretyping.expand_evars = true }
let refine_tac ist simple c =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let flags = constr_flags in
@@ -645,7 +645,7 @@ let subst_hole_with_term occ tc t =
open Tacmach
let hResolve id c occ t =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let sigma = Sigma.to_evar_map sigma in
let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
@@ -708,7 +708,7 @@ END
exception Found of unit Proofview.tactic
let rewrite_except h =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.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))
@@ -727,11 +727,11 @@ let refl_equal =
should be replaced by a call to the tactic but I don't know how to
call it before it is defined. *)
let mkCaseEq a : unit Proofview.tactic =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in
Tacticals.New.tclTHENLIST
[Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))];
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
(** FIXME: this looks really wrong. Does anybody really use this tactic? *)
@@ -743,16 +743,16 @@ let mkCaseEq a : unit Proofview.tactic =
let case_eq_intros_rewrite x =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in
(* Pp.msgnl (Printer.pr_lconstr x); *)
Tacticals.New.tclTHENLIST [
mkCaseEq x;
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let hyps = Tacmach.New.pf_ids_of_hyps gl in
let n' = nb_prod (Tacmach.New.project gl) concl in
- let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in
+ let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in
Tacticals.New.tclTHENLIST [
Tacticals.New.tclDO (n'-n-1) intro;
introduction h;
@@ -783,15 +783,15 @@ let destauto t =
with Found tac -> tac
let destauto_in id =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
(* Pp.msgnl (Printer.pr_lconstr (ctype)); *)
destauto ctype
end }
TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ]
+| [ "destauto" ] -> [ Proofview.Goal.enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ]
| [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
END
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index b7f0881f1..f47c03dfc 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -74,7 +74,7 @@ TACTIC EXTEND is_ground
END
TACTIC EXTEND autoapply
- [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply c i) ]
+ [ "autoapply" constr(c) "using" preident(i) ] -> [ autoapply c i ]
END
(** TODO: DEPRECATE *)
@@ -90,10 +90,10 @@ let rec eq_constr_mod_evars sigma x y =
| _, _ -> compare_constr sigma (fun x y -> eq_constr_mod_evars sigma x y) x y
let progress_evars t =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let check =
- Proofview.Goal.nf_enter { enter = begin fun gl' ->
+ Proofview.Goal.enter { enter = begin fun gl' ->
let sigma = Tacmach.New.project gl' in
let newconcl = Proofview.Goal.concl gl' in
if eq_constr_mod_evars sigma concl newconcl
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index bc57fcf56..810f02c4f 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1543,7 +1543,7 @@ let rec insert_dependent env sigma decl accu hyps = match hyps with
insert_dependent env sigma decl (ndecl :: accu) rem
let assert_replacing id newt tac =
- let prf = Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let prf = Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -1611,7 +1611,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
Proofview.Unsafe.tclEVARS undef <*>
convert_concl_no_check newt DEFAULTcast
in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -2095,7 +2095,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 ->
+ Proofview.Goal.enter { enter = begin fun gl ->
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
@@ -2129,7 +2129,7 @@ let not_declared env sigma ty rel =
str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
let setoid_proof ty fn fallback =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 62d0cc529..167501de2 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -844,10 +844,10 @@ let rec message_of_value v =
Ftactic.return (str "<tactic>")
else if has_type v (topwit wit_constr) then
let v = out_gen (topwit wit_constr) v in
- Ftactic.nf_enter {enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end }
+ Ftactic.enter {enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end }
else if has_type v (topwit wit_constr_under_binders) then
let c = out_gen (topwit wit_constr_under_binders) v in
- Ftactic.nf_enter { enter = begin fun gl ->
+ Ftactic.enter { enter = begin fun gl ->
Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c)
end }
else if has_type v (topwit wit_unit) then
@@ -860,21 +860,21 @@ let rec message_of_value v =
let (c, sigma) = Tactics.run_delayed env sigma c in
pr_econstr_env env sigma c
in
- Ftactic.nf_enter { enter = begin fun gl ->
+ Ftactic.enter { enter = begin fun gl ->
Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p)
end }
else if has_type v (topwit wit_constr_context) then
let c = out_gen (topwit wit_constr_context) v in
- Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end }
+ Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end }
else if has_type v (topwit wit_uconstr) then
let c = out_gen (topwit wit_uconstr) v in
- Ftactic.nf_enter { enter = begin fun gl ->
+ Ftactic.enter { enter = begin fun gl ->
Ftactic.return (pr_closed_glob_env (pf_env gl)
(project gl) c)
end }
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
- Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_id id) end }
+ Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_id id) end }
else match Value.to_list v with
| Some l ->
Ftactic.List.map message_of_value l >>= fun l ->
@@ -1213,7 +1213,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
end
| TacAbstract (tac,ido) ->
- Proofview.Goal.nf_enter { enter = begin fun gl -> Tactics.tclABSTRACT
+ Proofview.Goal.enter { enter = begin fun gl -> Tactics.tclABSTRACT
(Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac)
end }
| TacThen (t1,t) ->
@@ -1521,7 +1521,7 @@ and interp_match ist lz constr lmr =
(* Interprets the Match Context expressions *)
and interp_match_goal ist lz lr lmr =
- Ftactic.nf_enter { enter = begin fun gl ->
+ Ftactic.enter { enter = begin fun gl ->
let sigma = project gl in
let env = Proofview.Goal.env gl in
let hyps = Proofview.Goal.hyps gl in
@@ -1750,8 +1750,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(Tactics.generalize_gen cl)) sigma
end }
| TacLetTac (na,c,clp,b,eqpat) ->
- Proofview.V82.nf_evar_goals <*>
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
let clp = interp_clause ist env sigma clp in
@@ -1788,7 +1787,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacInductionDestruct (isrec,ev,(l,el)) ->
(* spiwack: some unknown part of destruct needs the goal to be
prenormalised. *)
- Proofview.V82.nf_evar_goals <*>
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
@@ -1824,8 +1822,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacChange (None,c,cl) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
- Proofview.V82.nf_evar_goals <*>
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let is_onhyps = match cl.onhyps with
| None | Some [] -> true
| _ -> false
@@ -1854,7 +1851,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacChange (Some op,c,cl) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
- Proofview.V82.nf_evar_goals <*>
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
@@ -1899,7 +1895,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
by))
end }
| TacInversion (DepInversion (k,c,ids),hyp) ->
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
let (sigma,c_interp) =
@@ -2050,7 +2046,7 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm
Sigma.Unsafe.of_pair (c, sigma)
}
-let interp_destruction_arg' ist c = Ftactic.nf_enter { enter = begin fun gl ->
+let interp_destruction_arg' ist c = Ftactic.enter { enter = begin fun gl ->
Ftactic.return (interp_destruction_arg ist gl c)
end }
@@ -2080,7 +2076,7 @@ let () =
register_interp0 wit_ltac interp
let () =
- register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl ->
+ register_interp0 wit_uconstr (fun ist c -> Ftactic.enter { enter = begin fun gl ->
Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) (Tacmach.New.project gl) c)
end })
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 5d894c677..c9c904e35 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -182,9 +182,10 @@ let litteral_of_constr env sigma term=
(* store all equalities from the context *)
let make_prb gls depth additionnal_terms =
+ let open Tacmach.New in
let env=pf_env gls in
- let sigma=sig_sig gls in
- let state = empty depth gls in
+ let sigma=project gls in
+ let state = empty depth {it = Proofview.Goal.goal (Proofview.Goal.assume gls); sigma } in
let pos_hyps = ref [] in
let neg_hyps =ref [] in
List.iter
@@ -196,7 +197,7 @@ let make_prb gls depth additionnal_terms =
let id = NamedDecl.get_id decl in
begin
let cid=Constr.mkVar id in
- match litteral_of_constr env sigma (EConstr.of_constr (NamedDecl.get_type decl)) with
+ match litteral_of_constr env sigma (NamedDecl.get_type decl) with
`Eq (t,a,b) -> add_equality state cid a b
| `Neq (t,a,b) -> add_disequality state (Hyp cid) a b
| `Other ph ->
@@ -213,7 +214,7 @@ let make_prb gls depth additionnal_terms =
neg_hyps:=(cid,nh):: !neg_hyps
| `Rule patts -> add_quant state id true patts
| `Nrule patts -> add_quant state id false patts
- end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it));
+ end) (Proofview.Goal.hyps gls);
begin
match atom_of_constr env sigma (pf_concl gls) with
`Eq (t,a,b) -> add_disequality state Goal a b
@@ -227,6 +228,7 @@ let make_prb gls depth additionnal_terms =
(* indhyps builds the array of arrays of constructor hyps for (ind largs) *)
let build_projection intype (cstr:pconstructor) special default gls=
+ let open Tacmach.New in
let ci= (snd(fst cstr)) in
let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
let id=pf_get_new_id (Id.of_string "t") gls in
@@ -266,7 +268,7 @@ let refresh_universes ty k =
let constr_of_term c = EConstr.of_constr (constr_of_term c)
let rec proof_tac p : unit Proofview.tactic =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
try (* type_of can raise exceptions *)
match p.p_rule with
@@ -296,7 +298,7 @@ let rec proof_tac p : unit Proofview.tactic =
refresh_universes (type_of tf1) (fun typf ->
refresh_universes (type_of tx1) (fun typx ->
refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
- let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
+ let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in
let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in
@@ -322,7 +324,7 @@ let rec proof_tac p : unit Proofview.tactic =
refresh_universes (type_of ti) (fun intype ->
refresh_universes (type_of default) (fun outtype ->
let proj =
- Tacmach.New.of_old (build_projection intype cstr special default) gl
+ build_projection intype cstr special default gl
in
let injt=
app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
@@ -331,9 +333,9 @@ let rec proof_tac p : unit Proofview.tactic =
end }
let refute_tac c t1 t2 p =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
- let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
+ let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
let false_t=mkApp (c,[|mkVar hid|]) in
let k intype =
let neweq= new_app_global _eq [|intype;tt1;tt2|] in
@@ -347,12 +349,12 @@ let refine_exact_check c gl =
Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
let convert_to_goal_tac c t1 t2 p =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let k sort =
let neweq= new_app_global _eq [|sort;tt1;tt2|] in
- let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
- let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+ let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in
+ let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
let identity=mkLambda (Name x,sort,mkRel 1) in
let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
@@ -361,9 +363,9 @@ let convert_to_goal_tac c t1 t2 p =
end }
let convert_to_hyp_tac c1 t1 c2 t2 p =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let tt2=constr_of_term t2 in
- let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
+ let h = Tacmach.New.pf_get_new_id (Id.of_string "H") gl in
let false_t=mkApp (c2,[|mkVar h|]) in
Tacticals.New.tclTHENS (assert_before (Name h) tt2)
[convert_to_goal_tac c1 t1 t2 p;
@@ -371,11 +373,11 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
end }
let discriminate_tac (cstr,u as cstru) p =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
- let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+ let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
let identity = Universes.constr_of_global (Lazy.force _I) in
let identity = EConstr.of_constr identity in
let trivial = Universes.constr_of_global (Lazy.force _True) in
@@ -385,8 +387,8 @@ let discriminate_tac (cstr,u as cstru) p =
let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
let outtype = mkSort outtype in
let pred = mkLambda(Name xid,outtype,mkRel 1) in
- let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
- let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in
+ let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
+ let proj = build_projection intype cstru trivial concl gl in
let injt=app_global _f_equal
[|intype;outtype;proj;t1;t2;mkVar hid|] in
let endt k =
@@ -409,11 +411,11 @@ let build_term_to_complete uf meta pac =
applist (mkConstructU cinfo.ci_constr, all_args)
let cc_tactic depth additionnal_terms =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
Coqlib.check_required_library Coqlib.logic_module_name;
let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
- let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
+ let state = make_prb gl depth additionnal_terms in
let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
let sol = execute true state in
let _ = debug (fun () -> Pp.str "Computation completed.") in
@@ -498,7 +500,7 @@ let mk_eq f c1 c2 k =
end })
let f_equal =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
let cut_eq c1 c2 =
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 72aeb9066..adf926958 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -38,7 +38,7 @@ open OmegaSolver
(* Added by JCF, 09/03/98 *)
let elim_id id =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
simplest_elim (Tacmach.New.pf_global id gl)
end }
let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
@@ -1391,7 +1391,10 @@ let normalize_equation sigma id flag theorem pos t t1 t2 (tactic,defs) =
else
(tactic,defs)
+let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c
+
let destructure_omega gl tac_def (id,c) =
+ let open Tacmach.New in
let sigma = project gl in
if String.equal (atompart_of_id id) "State" then
tac_def
@@ -1433,10 +1436,10 @@ let reintroduce id =
open Proofview.Notations
let coq_omega =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
clear_constr_tables ();
let hyps_types = Tacmach.New.pf_hyps_types gl in
- let destructure_omega = Tacmach.New.of_old destructure_omega gl in
+ let destructure_omega = destructure_omega gl in
let tactic_normalisation, system =
List.fold_left destructure_omega ([],[]) hyps_types in
let prelude,sys =
@@ -1486,7 +1489,7 @@ let coq_omega =
let coq_omega = coq_omega
let nat_inject =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in
let rec explore p t : unit Proofview.tactic =
Proofview.tclEVARMAP >>= fun sigma ->
@@ -1657,6 +1660,7 @@ let not_binop = function
exception Undecidable
let rec decidability gl t =
+ let open Tacmach.New in
match destructurate_prop (project gl) t with
| Kapp(Or,[t1;t2]) ->
mkApp (Lazy.force coq_dec_or, [| t1; t2;
@@ -1687,22 +1691,25 @@ let rec decidability gl t =
| Kapp(True,[]) -> Lazy.force coq_dec_True
| _ -> raise Undecidable
+let fresh_id avoid id gl =
+ fresh_id_in_env avoid id (Proofview.Goal.env gl)
+
let onClearedName id tac =
(* We cannot ensure that hyps can be cleared (because of dependencies), *)
(* so renaming may be necessary *)
Tacticals.New.tclTHEN
(Tacticals.New.tclTRY (clear [id]))
- (Proofview.Goal.nf_enter { enter = begin fun gl ->
- let id = Tacmach.New.of_old (fresh_id [] id) gl in
+ (Proofview.Goal.enter { enter = begin fun gl ->
+ let id = fresh_id [] id gl in
Tacticals.New.tclTHEN (introduction id) (tac id)
end })
let onClearedName2 id tac =
Tacticals.New.tclTHEN
(Tacticals.New.tclTRY (clear [id]))
- (Proofview.Goal.nf_enter { enter = begin fun gl ->
- let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in
- let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in
+ (Proofview.Goal.enter { enter = begin fun gl ->
+ let id1 = fresh_id [] (add_suffix id "_left") gl in
+ let id2 = fresh_id [] (add_suffix id "_right") gl in
Tacticals.New.tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
end })
@@ -1712,10 +1719,10 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with
| _ -> false
let destructure_hyps =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
- let decidability = Tacmach.New.of_old decidability gl in
- let pf_nf = Tacmach.New.of_old pf_nf gl in
+ let decidability = decidability gl in
+ let pf_nf = pf_nf gl in
let rec loop = function
| [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
| decl::lit ->
@@ -1854,9 +1861,9 @@ let destructure_hyps =
end }
let destructure_goal =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
- let decidability = Tacmach.New.of_old decidability gl in
+ let decidability = decidability gl in
let rec loop t =
Proofview.tclEVARMAP >>= fun sigma ->
let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5645850b2..f9ebc4233 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -129,11 +129,13 @@ let mk_clenv_from_env env sigma n (c,cty) =
env = env }
let mk_clenv_from_n gls n (c,cty) =
- mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty)
+ let env = Proofview.Goal.env gls in
+ let sigma = Tacmach.New.project gls in
+ mk_clenv_from_env env sigma 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,Tacmach.New.pf_unsafe_type_of gls t)
(******************************************************************)
@@ -263,8 +265,7 @@ let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
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 clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then
clenv_unify CUMUL ~flags (clenv_type clenv) concl
(clenv_unify_meta_types ~flags clenv)
@@ -272,6 +273,14 @@ let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
clenv_unify CUMUL ~flags
(meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
+let old_clenv_unique_resolver ?flags clenv gl =
+ let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+ clenv_unique_resolver_gen ?flags clenv concl
+
+let clenv_unique_resolver ?flags clenv gl =
+ let concl = Proofview.Goal.concl gl in
+ clenv_unique_resolver_gen ?flags clenv concl
+
let adjust_meta_source evd mv = function
| loc,Evar_kinds.VarInstance id ->
let rec match_name c l =
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index f7ff4bed3..4bcd50591 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -41,10 +41,10 @@ val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr
(** type of a meta in clenv context *)
val clenv_meta_type : clausenv -> metavariable -> types
-val mk_clenv_from : Goal.goal sigma -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_from : ('a, 'r) Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
val mk_clenv_from_n :
- Goal.goal sigma -> int option -> EConstr.constr * EConstr.types -> clausenv
-val mk_clenv_type_of : Goal.goal sigma -> EConstr.constr -> clausenv
+ ('a, 'r) Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> clausenv
val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
(** Refresh the universes in a clenv *)
@@ -62,9 +62,12 @@ val clenv_unify :
?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
(** unifies the concl of the goal with the type of the clenv *)
-val clenv_unique_resolver :
+val old_clenv_unique_resolver :
?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
+val clenv_unique_resolver :
+ ?flags:unify_flags -> clausenv -> ('a, 'r) Proofview.Goal.t -> clausenv
+
val clenv_dependent : clausenv -> metavariable list
val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 32c887ff5..0722ea047 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -105,8 +105,8 @@ let dft = default_unify_flags
let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
Proofview.Goal.enter { enter = begin fun gl ->
- let clenv gl = clenv_unique_resolver ~flags clenv gl in
- clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
+ let clenv = clenv_unique_resolver ~flags clenv gl in
+ clenv_refine with_evars ~with_classes clenv
end }
(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b548f8b92..c8c119aee 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -101,9 +101,9 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
in clenv, c
let unify_resolve poly flags ((c : raw_hint), clenv) =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let clenv, c = connect_hint_clenv poly c clenv gl in
- let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in
+ let clenv = clenv_unique_resolver ~flags clenv gl in
Clenvtac.clenv_refine false clenv
end }
@@ -330,7 +330,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
end })
in
Proofview.Goal.enter { enter = begin fun gl ->
- let concl = Tacmach.New.pf_nf_concl gl in
+ let concl = Tacmach.New.pf_concl gl in
let sigma = Tacmach.New.project gl in
let secvars = compute_secvars gl in
Tacticals.New.tclFIRST
@@ -421,7 +421,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
"nocore" amongst the databases. *)
let trivial ?(debug=Off) lems dbnames =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let db_list = make_db_list dbnames in
@@ -432,7 +432,7 @@ let trivial ?(debug=Off) lems dbnames =
end }
let full_trivial ?(debug=Off) lems =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let db_list = current_pure_db () in
@@ -490,7 +490,7 @@ let search d n mod_delta db_list local_db =
Tacticals.New.tclORELSE0 (dbg_assumption d)
(Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
( Proofview.Goal.enter { enter = begin fun gl ->
- let concl = Tacmach.New.pf_nf_concl gl in
+ let concl = Tacmach.New.pf_concl gl in
let sigma = Tacmach.New.project gl in
let secvars = compute_secvars gl in
let d' = incr_dbg d in
@@ -506,7 +506,7 @@ let search d n mod_delta db_list local_db =
let default_search_depth = ref 5
let delta_auto debug mod_delta n lems dbnames =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let db_list = make_db_list dbnames in
@@ -529,7 +529,7 @@ let new_auto ?(debug=Off) n = delta_auto debug true n
let default_auto = auto !default_search_depth [] []
let delta_full_auto ?(debug=Off) mod_delta n lems =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let db_list = current_pure_db () in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index f43f4b250..e58ec5a31 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -92,7 +92,7 @@ type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.
let one_base general_rewrite_maybe_in tac_main bas =
let lrul = find_rewrites bas in
let try_rewrite dir ctx c tc =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
let c' = Vars.subst_univs_level_constr subst c in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 669d80814..8ada9e6a7 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -231,13 +231,13 @@ let e_give_exact flags poly (c,clenv) gl =
let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
let clenv', c = connect_hint_clenv poly c clenv gls in
- let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+ let clenv' = clenv_unique_resolver ~flags clenv' gls in
Clenvtac.clenv_refine true ~with_classes:false clenv'
end }
let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
let clenv', _ = connect_hint_clenv poly c clenv gls in
- let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+ let clenv' = clenv_unique_resolver ~flags clenv' gls in
Clenvtac.clenv_refine false ~with_classes:false clenv'
end }
@@ -285,16 +285,16 @@ let clenv_of_prods poly nprods (c, clenv) gl =
if Pervasives.(>=) diff 0 then
(* Was Some clenv... *)
Some (Some diff,
- Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
+ mk_clenv_from_n gl (Some diff) (c,ty))
else None
let with_prods nprods poly (c, clenv) f =
if get_typeclasses_limit_intros () then
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
match clenv_of_prods poly nprods (c, clenv) gl with
| None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
| Some (diff, clenv') -> f.enter gl (c, diff, clenv') end }
- else Proofview.Goal.nf_enter
+ else Proofview.Goal.enter
{ enter = begin fun gl ->
if Int.equal nprods 0 then f.enter gl (c, None, clenv)
else Tacticals.New.tclZEROMSG (str"Not enough premisses") end }
@@ -345,7 +345,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
let open Tacticals.New in
let open Tacmach.New in
let trivial_fail =
- Proofview.Goal.nf_enter { enter =
+ Proofview.Goal.enter { enter =
begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -356,7 +356,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
end }
in
let trivial_resolve =
- Proofview.Goal.nf_enter { enter =
+ Proofview.Goal.enter { enter =
begin fun gl ->
let tacs = e_trivial_resolve db_list local_db secvars only_classes
(project gl) (pf_concl gl) in
@@ -944,7 +944,7 @@ module Search = struct
Hint_db.transparent_state cached_hints == st
then cached_hints
else
- let hints = make_hints {it = Goal.goal g; sigma = project g}
+ let hints = make_hints {it = Goal.goal (Proofview.Goal.assume g); sigma = project g}
st only_classes sign
in
autogoal_cache := (cwd, only_classes, sign, hints); hints
@@ -1024,16 +1024,16 @@ module Search = struct
(pr_depth (!idx :: info.search_depth) ++ str": trying " ++
Lazy.force pp ++
(if !foundone != true then
- str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl)
+ str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal (Proofview.Goal.assume gl))
else mt ())));
- let tac_of gls i j = Goal.nf_enter { enter = fun gl' ->
+ let tac_of gls i j = Goal.enter { enter = fun gl' ->
let sigma' = Goal.sigma gl' in
let s' = Sigma.to_evar_map sigma' in
let _concl = Goal.concl gl' in
if !typeclasses_debug > 0 then
Feedback.msg_debug
(pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++
- pr_ev s' (Proofview.Goal.goal gl'));
+ pr_ev s' (Proofview.Goal.goal (Proofview.Goal.assume gl')));
let eq c1 c2 = EConstr.eq_constr s' c1 c2 in
let hints' =
if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl))
@@ -1042,7 +1042,7 @@ module Search = struct
make_autogoal_hints info.search_only_classes ~st gl'
else info.search_hints
in
- let dep' = info.search_dep || Proofview.unifiable s' (Goal.goal gl') gls in
+ let dep' = info.search_dep || Proofview.unifiable s' (Goal.goal (Proofview.Goal.assume gl')) gls in
let info' =
{ search_depth = succ j :: i :: info.search_depth;
last_tac = pp;
@@ -1059,7 +1059,7 @@ module Search = struct
(if !typeclasses_debug > 0 then
Feedback.msg_debug
(pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp
- ++ str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl)
+ ++ str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal (Proofview.Goal.assume gl))
++ str", " ++ int j ++ str" subgoal(s)" ++
(Option.cata (fun k -> str " in addition to the first " ++ int k)
(mt()) k)));
@@ -1130,7 +1130,7 @@ module Search = struct
else tclONCE (aux (NotApplicableEx,Exninfo.null) poss)
let hints_tac hints info kont : unit Proofview.tactic =
- Proofview.Goal.nf_enter
+ Proofview.Goal.enter
{ enter = fun gl -> hints_tac_gl hints info kont gl }
let intro_tac info kont gl =
@@ -1150,7 +1150,7 @@ module Search = struct
let intro info kont =
Proofview.tclBIND Tactics.intro
- (fun _ -> Proofview.Goal.nf_enter { enter = fun gl -> intro_tac info kont gl })
+ (fun _ -> Proofview.Goal.enter { enter = fun gl -> intro_tac info kont gl })
let rec search_tac hints limit depth =
let kont info =
@@ -1173,7 +1173,7 @@ module Search = struct
unit Proofview.tactic =
let open Proofview in
let open Proofview.Notations in
- let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
+ let dep = dep || Proofview.unifiable sigma (Goal.goal (Proofview.Goal.assume gl)) gls in
let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
search_tac hints depth 1 info
@@ -1510,11 +1510,11 @@ let is_ground c gl =
if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
else tclFAIL 0 (str"Not ground") gl
-let autoapply c i gl =
+let autoapply c i = Proofview.Goal.enter { enter = begin fun 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 c in
+ let cty = Tacmach.New.pf_unsafe_type_of gl c in
let ce = mk_clenv_from gl (c,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
+ (unify_e_resolve false flags).enter gl
+ ((c,cty,Univ.ContextSet.empty),0,ce)
+end }
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 171b5c4ea..8855093ee 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -31,7 +31,7 @@ val not_evar : constr -> unit Proofview.tactic
val is_ground : constr -> tactic
-val autoapply : constr -> Hints.hint_db_name -> tactic
+val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
module Search : sig
val eauto_tac :
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 0e28aa980..63f923dfd 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -110,7 +110,7 @@ let is_negation_of env sigma typ t =
| _ -> false
let contradiction_term (c,lbind as cl) =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let type_of = Tacmach.New.pf_unsafe_type_of gl in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 7453fff5c..14082bb8d 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -112,13 +112,12 @@ open Auto
let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
let unify_e_resolve poly flags (c,clenv) =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let clenv', c = connect_hint_clenv poly c clenv gl in
- Proofview.V82.tactic
- (fun gls ->
- let clenv' = clenv_unique_resolver ~flags clenv' gls in
- tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
- (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
+ let clenv' = clenv_unique_resolver ~flags clenv' gl in
+ Proofview.tclTHEN
+ (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+ (Tactics.Simple.eapply c)
end }
let hintmap_of sigma secvars hdc concl =
@@ -139,7 +138,7 @@ let e_exact poly flags (c,clenv) =
end }
let rec e_trivial_fail_db db_list local_db =
- let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let next = Proofview.Goal.enter { enter = begin fun gl ->
let d = Tacmach.New.pf_last_hyp gl in
let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in
e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db)
@@ -149,7 +148,7 @@ let rec e_trivial_fail_db db_list local_db =
let tacl =
registered_e_assumption ::
(Tacticals.New.tclTHEN Tactics.intro next) ::
- (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
+ (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
in
Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
end }
@@ -501,7 +500,7 @@ let unfold_head env sigma (ids, csts) c =
in aux c
let autounfold_one db cl =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
diff --git a/tactics/elim.ml b/tactics/elim.ml
index a4158f821..e37ec6bce 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -133,7 +133,7 @@ let induction_trailer abs_i abs_j bargs =
(tclDO (abs_j - abs_i) intro)
(onLastHypId
(fun id ->
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let idty = pf_unsafe_type_of gl (mkVar id) in
let fvty = global_vars (pf_env gl) (project gl) idty in
let possible_bring_hyps =
@@ -155,7 +155,7 @@ let induction_trailer abs_i abs_j bargs =
))
let double_ind h1 h2 =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let abs_i = depth_of_quantified_hypothesis true h1 gl in
let abs_j = depth_of_quantified_hypothesis true h2 gl in
let abs =
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index df60f2c66..bac3980d2 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -176,7 +176,7 @@ let solveEqBranch rectype =
Proofview.tclORELSE
begin
Proofview.Goal.enter { enter = begin fun gl ->
- let concl = pf_nf_concl gl in
+ let concl = pf_concl gl in
let sigma = project gl in
match_eqdec sigma concl >>= fun (eqonleft,op,lhs,rhs,_) ->
let (mib,mip) = Global.lookup_inductive rectype in
@@ -202,7 +202,7 @@ let decideGralEquality =
Proofview.tclORELSE
begin
Proofview.Goal.enter { enter = begin fun gl ->
- let concl = pf_nf_concl gl in
+ let concl = pf_concl gl in
let sigma = project gl in
match_eqdec sigma concl >>= fun (eqonleft,_,c1,c2,typ) ->
let headtyp = hd_app sigma (pf_compute gl typ) in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d9b668517..6fcf529c2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -306,7 +306,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
else instantiate_lemma_all frzevars gl c t l l2r concl
in
let typ = match cls with
- | None -> pf_nf_concl gl
+ | None -> pf_concl gl
| Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl)
in
let cs = instantiate_lemma typ in
@@ -406,7 +406,7 @@ let type_of_clause cls gl = match cls with
| Some id -> pf_get_hyp_typ id gl
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 ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let evd = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
let isatomic = isProd evd (whd_zeta evd hdcncl) in
let dep_fun = if isatomic then dependent else dependent_no_evar in
@@ -1009,7 +1009,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
match find_positions env sigma t1 t2 with
| Inr _ ->
@@ -1019,7 +1019,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
end }
let onEquality with_evars tac (c,lbindc) =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
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 c in
@@ -1034,7 +1034,7 @@ let onEquality with_evars tac (c,lbindc) =
end }
let onNegatedEquality with_evars tac =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
let ccl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
@@ -1302,7 +1302,7 @@ let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
let inject_if_homogenous_dependent_pair ty =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
try
let sigma = Tacmach.New.project gl in
let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
@@ -1458,7 +1458,7 @@ let injConcl = injClause None false None
let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id)))
let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = clause.evd in
let env = Proofview.Goal.env gl in
match find_positions env sigma t1 t2 with
@@ -1567,7 +1567,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
(* on for further iterated sigma-tuples *)
let cutSubstInConcl l2r eqn =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.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
@@ -1586,7 +1586,7 @@ let cutSubstInConcl l2r eqn =
end }
let cutSubstInHyp l2r eqn id =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.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
@@ -1812,7 +1812,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
Proofview.tclUNIT ()
end }
in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let ids = find_equations gl in
tclMAP process ids
end }
@@ -1822,7 +1822,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
(* Old implementation, not able to manage configurations like a=b, a=t,
or situations like "a = S b, b = S a", or also accidentally unfolding
let-ins *)
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = project gl in
let find_eq_data_decompose = find_eq_data_decompose gl in
let test (_,c) =
@@ -1877,7 +1877,7 @@ let rewrite_assumption_cond cond_eq_term cl =
with | Failure _ | UserError _ -> arec rest gl
end
in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.lift gl Sigma.Unsafe.le in
let hyps = Proofview.Goal.hyps gl in
arec hyps gl
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 632a29721..904a17417 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -273,7 +273,7 @@ Nota: with Inversion_clear, only four useless hypotheses
let generalizeRewriteIntros as_mode tac depids id =
Proofview.tclENV >>= fun env ->
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let dids = dependent_hyps env id depids gl in
let reintros = if as_mode then intros_replacing else intros_possibly_replacing in
(tclTHENLIST
@@ -342,7 +342,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
(if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
in
let substHypIfVariable tac id =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = project gl in
(** We only look at the type of hypothesis "id" *)
let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
@@ -378,7 +378,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
id
let nLastDecls i tac =
- Proofview.Goal.nf_enter { enter = begin fun gl -> tac (nLastDecls gl i) end }
+ Proofview.Goal.enter { enter = begin fun gl -> tac (nLastDecls gl i) end }
(* Introduction of the equations on arguments
othin: discriminates Simple Inversion, Inversion and Inversion_clear
@@ -386,7 +386,7 @@ let nLastDecls i tac =
Some thin: the equations are rewritten, and cleared if thin is true *)
let rewrite_equations as_mode othin neqns names ba =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
let first_eq = ref MoveLast in
let avoid = if as_mode then List.map NamedDecl.get_id nodepids else [] in
@@ -436,7 +436,7 @@ let rewrite_equations_tac as_mode othin id neqns names ba =
tac
let raw_inversion inv_kind id status names =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let sigma = Sigma.to_evar_map sigma in
let env = Proofview.Goal.env gl in
@@ -517,14 +517,14 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
* back to their places in the hyp-list. *)
let invIn k names ids id =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
let concl = Proofview.Goal.concl gl in
let sigma = project gl in
let nb_prod_init = nb_prod sigma concl in
let intros_replace_ids =
Proofview.Goal.enter { enter = begin fun gl ->
- let concl = pf_nf_concl gl in
+ let concl = pf_concl gl in
let sigma = project gl in
let nb_of_new_hyp =
nb_prod sigma concl - (List.length hyps + nb_prod_init)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index d864e547c..daa962f1d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -262,7 +262,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 open Tacmach in
+ let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in
let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
with
@@ -277,7 +278,7 @@ let lemInv id c gls =
let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
let lemInvIn id c ids =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
let intros_replace_ids =
let concl = Proofview.Goal.concl gl in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 94f22f903..27c1987a0 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -267,40 +267,6 @@ let pf_with_evars glsev k gls =
let pf_constr_of_global gr k =
pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k
-(* computing the case/elim combinators *)
-
-let gl_make_elim ind gl =
- let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
- let (sigma, c) = pf_apply Evd.fresh_global gl gr in
- (sigma, EConstr.of_constr c)
-
-let gl_make_case_dep ind gl =
- let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
- let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
- (elimination_sort_of_goal gl)
- in
- (Sigma.to_evar_map sigma, EConstr.of_constr r)
-
-let gl_make_case_nodep ind gl =
- let sigma = Sigma.Unsafe.of_evar_map (Tacmach.project gl) in
- let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
- (elimination_sort_of_goal gl)
- in
- (Sigma.to_evar_map sigma, EConstr.of_constr r)
-
-let make_elim_branch_assumptions ba gl =
- let assums =
- try List.rev (List.firstn ba.nassums (pf_hyps gl))
- with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
- { ba = ba; assums = assums }
-
-let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl
-
-let make_case_branch_assumptions = make_elim_branch_assumptions
-
-let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl
-
-
(** Tacticals of Ltac defined directly in term of Proofview *)
module New = struct
open Proofview
@@ -534,7 +500,7 @@ module New = struct
Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
let tclDELAYEDWITHHOLES check x tac =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let Sigma (x, sigma, _) = x.delayed env sigma in
@@ -578,13 +544,13 @@ module New = struct
let onLastHyp = onNthHyp 1
let onNthDecl m tac =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
Proofview.tclUNIT (nthDecl m gl) >>= tac
end }
let onLastDecl = onNthDecl 1
let ifOnHyp pred tac1 tac2 id =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let typ = Tacmach.New.pf_get_hyp_typ id gl in
if pred (id,typ) then
tac1 id
@@ -592,7 +558,7 @@ module New = struct
tac2 id
end }
- let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find.enter gl) end }
+ let onHyps find tac = Proofview.Goal.enter { enter = begin fun gl -> tac (find.enter gl) end }
let afterHyp id tac =
Proofview.Goal.enter { enter = begin fun gl ->
@@ -625,13 +591,13 @@ 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) =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let sigma, elim = (mk_elim ind).enter 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
+ (Proofview.Goal.enter { enter = begin fun gl ->
+ let indclause = mk_clenv_from gl (c, t) 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 elim)) gl in
+ let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim) in
let indmv =
match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
| Meta mv -> mv
@@ -660,7 +626,7 @@ module New = struct
| None -> elimclause'
| Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
in
- let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in
+ let clenv' = clenv_unique_resolver ~flags elimclause' gl in
let after_tac i =
let (hd,largs) = decompose_app clenv'.evd clenv'.templtyp.Evd.rebus in
let ba = { branchsign = branchsigns.(i);
@@ -679,8 +645,64 @@ module New = struct
(Proofview.tclEXTEND [] tclIDTAC branchtacs)
end }) end }
+ let elimination_sort_of_goal gl =
+ (** Retyping will expand evars anyway. *)
+ let c = Proofview.Goal.concl (Goal.assume gl) in
+ pf_apply Retyping.get_sort_family_of gl c
+
+ let elimination_sort_of_hyp id gl =
+ (** Retyping will expand evars anyway. *)
+ let c = pf_get_hyp_typ id (Goal.assume gl) in
+ pf_apply Retyping.get_sort_family_of gl c
+
+ let elimination_sort_of_clause id gl = match id with
+ | None -> elimination_sort_of_goal gl
+ | Some id -> elimination_sort_of_hyp id gl
+
+ (* computing the case/elim combinators *)
+
+ let gl_make_elim ind = { enter = begin fun gl ->
+ let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
+ let (sigma, c) = pf_apply Evd.fresh_global gl gr in
+ (sigma, EConstr.of_constr c)
+ end }
+
+ let gl_make_case_dep ind = { enter = begin fun gl ->
+ let sigma = Sigma.Unsafe.of_evar_map (project gl) in
+ let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind true
+ (elimination_sort_of_goal gl)
+ in
+ (Sigma.to_evar_map sigma, EConstr.of_constr r)
+ end }
+
+ let gl_make_case_nodep ind = { enter = begin fun gl ->
+ let sigma = Sigma.Unsafe.of_evar_map (project gl) in
+ let Sigma (r, sigma, _) = Indrec.build_case_analysis_scheme (pf_env gl) sigma ind false
+ (elimination_sort_of_goal gl)
+ in
+ (Sigma.to_evar_map sigma, EConstr.of_constr r)
+ end }
+
+ let make_elim_branch_assumptions ba hyps =
+ let assums =
+ try List.rev (List.firstn ba.nassums hyps)
+ with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions") in
+ { ba = ba; assums = assums }
+
+ let elim_on_ba tac ba =
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+ tac branches
+ end }
+
+ let case_on_ba tac ba =
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+ tac branches
+ end }
+
let elimination_then tac c =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
let isrec,mkelim =
match (Global.lookup_mind (fst (fst ind))).mind_record with
@@ -696,34 +718,8 @@ module New = struct
let case_nodep_then_using =
general_elim_then_using gl_make_case_nodep false
- let elim_on_ba tac ba =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in
- tac branches
- end }
-
- let case_on_ba tac ba =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in
- tac branches
- end }
-
- let elimination_sort_of_goal gl =
- (** Retyping will expand evars anyway. *)
- let c = Proofview.Goal.concl (Goal.assume gl) in
- pf_apply Retyping.get_sort_family_of gl c
-
- let elimination_sort_of_hyp id gl =
- (** Retyping will expand evars anyway. *)
- let c = pf_get_hyp_typ id (Goal.assume gl) in
- pf_apply Retyping.get_sort_family_of gl c
-
- let elimination_sort_of_clause id gl = match id with
- | None -> elimination_sort_of_goal gl
- | Some id -> elimination_sort_of_hyp id gl
-
let pf_constr_of_global ref tac =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let (sigma, c) = Evd.fresh_global env sigma ref in
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 4bb745875..c9ff77716 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -137,9 +137,6 @@ val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family
val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
-val elim_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic
-val case_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic
-
(** Tacticals defined directly in term of Proofview *)
(** The tacticals in the module [New] are the tactical of Ltac. Their
@@ -240,7 +237,7 @@ module New : sig
val onLastHyp : (constr -> unit tactic) -> unit tactic
val onLastDecl : (named_declaration -> unit tactic) -> unit tactic
- val onHyps : ([ `NF ], named_context) Proofview.Goal.enter ->
+ val onHyps : ([ `LZ ], named_context) Proofview.Goal.enter ->
(named_context -> unit tactic) -> unit tactic
val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 13ffbc52f..5ad43a7d6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -515,7 +515,7 @@ let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast
| _ -> error "Not enough products."
(* Refine as a fixpoint *)
-let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
+let mutual_fix f n rest j = Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
@@ -571,7 +571,7 @@ let rec check_is_mutcoind env sigma cl =
error "All methods must construct elements in coinductive types."
(* Refine as a cofixpoint *)
-let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl ->
+let mutual_cofix f others j = Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
@@ -697,12 +697,12 @@ let bind_red_expr_occurrences occs nbcl redexp =
certain hypothesis *)
let reduct_in_concl (redfun,sty) =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty
end }
let reduct_in_hyp ?(check=false) redfun (id,where) =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl)
end }
@@ -731,14 +731,14 @@ let pf_e_reduce_decl redfun where decl gl =
Sigma (LocalDef (id, b', ty'), sigma, p +> q)
let e_reduct_in_concl ~check (redfun, sty) =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let Sigma (c', sigma, p) = redfun.e_redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
Sigma (convert_concl ~check c' sty, sigma, p)
end }
let e_reduct_in_hyp ?(check=false) redfun (id, where) =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let Sigma (decl', sigma, p) = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in
Sigma (convert_hyp ~check decl', sigma, p)
end }
@@ -1112,7 +1112,7 @@ let depth_of_quantified_hypothesis red h gl =
str".")
let intros_until_gen red h =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let n = depth_of_quantified_hypothesis red h gl in
Tacticals.New.tclDO n (if red then introf else intro)
end }
@@ -1226,7 +1226,7 @@ let cut c =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
- let concl = Tacmach.New.pf_nf_concl gl in
+ let concl = Proofview.Goal.concl gl in
let is_sort =
try
(** Backward compat: ensure that [c] is well-typed. *)
@@ -1360,7 +1360,7 @@ let enforce_prop_bound_names rename tac =
mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t')
| _ -> assert false in
let rename_branch i =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let t = Proofview.Goal.concl gl in
@@ -1438,7 +1438,7 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
(* Case analysis tactics *)
let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
@@ -1629,7 +1629,7 @@ let make_projection env sigma params cstr sign elim i n c u =
in elim
let descend_in_conjunctions avoid tac (err, info) c =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
try
@@ -1676,7 +1676,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
(****************************************************)
let solve_remaining_apply_goals =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
if !apply_solve_class_goals then
try
@@ -1701,7 +1701,7 @@ let tclORELSEOPT t k =
| Some tac -> tac)
let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : EConstr.constr with_bindings)) =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
let flags =
@@ -1854,7 +1854,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
let apply_in_once sidecond_first with_delta with_destruct with_evars naming
id (clear_flag,(loc,(d,lbind))) tac =
let open Context.Rel.Declaration in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let flags =
@@ -1915,7 +1915,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
*)
let cut_and_apply c =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
match EConstr.kind sigma (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
| Prod (_,c1,c2) when Vars.noccurn sigma 1 c2 ->
@@ -1969,7 +1969,7 @@ let native_cast_no_check c = cast_no_check Term.NATIVEcast c
let exact_proof c =
let open Tacmach.New in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
Refine.refine { run = begin fun sigma ->
let sigma = Sigma.to_evar_map sigma in
let (c, ctx) = Constrintern.interp_casted_constr (pf_env gl) sigma c (pf_concl gl) in
@@ -2005,7 +2005,7 @@ let assumption =
let hyps = Proofview.Goal.hyps gl in
arec gl true hyps
end } in
- Proofview.Goal.nf_enter assumption_tac
+ Proofview.Goal.enter assumption_tac
(*****************************************************************)
(* Modification of a local context *)
@@ -2110,7 +2110,7 @@ let rec intros_clearing = function
(* Keeping only a few hypotheses *)
let keep hyps =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
Proofview.tclENV >>= fun env ->
let ccl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
@@ -2158,7 +2158,7 @@ let bring_hyps hyps =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let store = Proofview.Goal.extra gl in
- let concl = Tacmach.New.pf_nf_concl gl in
+ let concl = Tacmach.New.pf_concl gl in
let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
let args = Array.of_list (Context.Named.to_instance mkVar hyps) in
Refine.refine { run = begin fun sigma ->
@@ -2192,7 +2192,7 @@ let check_number_of_constructors expctdnumopt i nconstr =
let constructor_tac with_evars expctdnumopt i lbind =
Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
- let cl = Tacmach.New.pf_nf_concl gl in
+ let cl = Tacmach.New.pf_concl gl in
let reduce_to_quantified_ind =
Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
in
@@ -2231,7 +2231,7 @@ let any_constructor with_evars tacopt =
let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in
Proofview.Goal.enter { enter = begin fun gl ->
- let cl = Tacmach.New.pf_nf_concl gl in
+ let cl = Tacmach.New.pf_concl gl in
let reduce_to_quantified_ind =
Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
in
@@ -2291,7 +2291,7 @@ let my_find_eq_data_decompose gl t =
| Constr_matching.PatternMatchingFailure -> None
let intro_decomp_eq loc l thin tac id =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let c = mkVar id in
let t = Tacmach.New.pf_unsafe_type_of gl c in
let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
@@ -2702,7 +2702,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
Sigma (mkNamedLetIn id c t x, sigma, p)
let letin_tac with_eq id c ty occs =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let ccl = Proofview.Goal.concl gl in
@@ -2719,7 +2719,7 @@ let letin_tac with_eq id c ty occs =
end }
let letin_pat_tac with_eq id c occs =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let ccl = Proofview.Goal.concl gl in
@@ -2805,6 +2805,12 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
let sigma, t = Typing.type_of env sigma c in
generalize_goal_gen env sigma ids i o t cl
+let new_generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
+ let env = Tacmach.New.pf_env gl in
+ let ids = Tacmach.New.pf_ids_of_hyps gl in
+ let sigma, t = Typing.type_of env sigma c in
+ generalize_goal_gen env sigma ids i o t cl
+
let old_generalize_dep ?(with_let=false) c gl =
let env = pf_env gl in
let sign = pf_hyps gl in
@@ -2849,10 +2855,10 @@ let generalize_dep ?(with_let = false) c =
Proofview.V82.tactic (old_generalize_dep ~with_let c)
(** *)
-let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+let generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let newcl, evd =
- List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr
+ List.fold_right_i (new_generalize_goal gl) 0 lconstr
(Tacmach.New.pf_concl gl,Tacmach.New.project gl)
in
let (evd, _) = Typing.type_of env evd newcl in
@@ -3618,14 +3624,15 @@ let is_defined_variable env id =
env |> lookup_named id |> is_local_def
let abstract_args gl generalize_vars dep id defined f args =
+ let open Tacmach.New in
let open Context.Rel.Declaration in
- let sigma = ref (Tacmach.project gl) in
- let env = Tacmach.pf_env gl in
- let concl = Tacmach.pf_concl gl in
+ let sigma = ref (Tacmach.New.project gl) in
+ let env = Tacmach.New.pf_env gl in
+ let concl = Tacmach.New.pf_concl gl in
let dep = dep || local_occur_var !sigma id concl in
let avoid = ref [] in
let get_id name =
- let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in
+ let id = new_fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in
avoid := id :: !avoid; id
in
(* Build application generalized w.r.t. the argument plus the necessary eqs.
@@ -3640,7 +3647,7 @@ let abstract_args gl generalize_vars dep id defined f args =
let decl = List.hd rel in
RelDecl.get_name decl, RelDecl.get_type decl, c
in
- let argty = Tacmach.pf_unsafe_type_of gl arg in
+ let argty = Tacmach.New.pf_unsafe_type_of gl arg in
let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
let () = sigma := sigma' in
let lenctx = List.length ctx in
@@ -3681,7 +3688,7 @@ let abstract_args gl generalize_vars dep id defined f args =
true, mkApp (f', before), after
in
if dogen then
- let tyf' = Tacmach.pf_unsafe_type_of gl f' in
+ let tyf' = Tacmach.New.pf_unsafe_type_of gl f' in
let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
in
@@ -3689,14 +3696,14 @@ let abstract_args gl generalize_vars dep id defined f args =
let vars =
if generalize_vars then
let nogen = Id.Set.add id nogen in
- hyps_of_vars (pf_env gl) (project gl) (pf_hyps gl) nogen vars
+ hyps_of_vars (pf_env gl) (project gl) (Proofview.Goal.hyps gl) nogen vars
else []
in
let body, c' =
if defined then Some c', Retyping.get_type_of ctxenv !sigma c'
else None, c'
in
- let typ = Tacmach.pf_get_hyp_typ gl id in
+ let typ = Tacmach.New.pf_get_hyp_typ id gl in
let tac = make_abstract_generalize (pf_env gl) id typ concl dep ctx body c' eqs args refls in
let tac = Proofview.Unsafe.tclEVARS !sigma <*> tac in
Some (tac, dep, succ (List.length ctx), vars)
@@ -3704,7 +3711,7 @@ let abstract_args gl generalize_vars dep id defined f args =
let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
let open Context.Named.Declaration in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
Coqlib.check_required_library Coqlib.jmeq_module_name;
let sigma = Tacmach.New.project gl in
let (f, args, def, id, oldid) =
@@ -3719,7 +3726,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
if List.is_empty args then Proofview.tclUNIT ()
else
let args = Array.of_list args in
- let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in
+ let newc = abstract_args gl generalize_vars force_dep id def f args in
match newc with
| None -> Proofview.tclUNIT ()
| Some (tac, dep, n, vars) ->
@@ -3799,7 +3806,7 @@ let specialize_eqs id gl =
else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
-let specialize_eqs id = Proofview.Goal.nf_enter { enter = begin fun gl ->
+let specialize_eqs id = Proofview.Goal.enter { enter = begin fun gl ->
let msg = str "Specialization not allowed on dependent hypotheses" in
Proofview.tclOR (clear [id])
(fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () ->
@@ -4123,7 +4130,7 @@ 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 indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from_n gl (Some 0) (x,y)) gl in
+ let indclause = mk_clenv_from_n gl (Some 0) (x,y) in
let elimclause' = clenv_fchain ~with_univs:false i acc indclause in
elimclause')
(List.rev clauses)
@@ -4134,18 +4141,18 @@ let recolle_clenv i params args elimclause gl =
produce new ones). Then refine with the resulting term with holes.
*)
let induction_tac with_evars params indvars elim =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Tacmach.New.project gl in
let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in
let i = match i with None -> index_of_ind_arg sigma elimt | Some i -> i in
(* elimclause contains this: (elimc ?i ?j ?k...?l) *)
let elimc = contract_letin_in_lam_header sigma elimc in
let elimc = mkCast (elimc, DEFAULTcast, elimt) in
- let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
+ let elimclause = Tacmach.New.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
(* one last resolution (useless?) *)
- let resolved = Tacmach.New.of_old (clenv_unique_resolver ~flags:(elim_flags ()) elimclause') gl in
+ let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved)
end }
@@ -4158,7 +4165,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let sigma = Sigma.to_evar_map sigma in
- let concl = Tacmach.New.pf_nf_concl gl in
+ let concl = Tacmach.New.pf_concl gl in
let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env sigma in
let dep_in_concl = Option.cata (fun id -> occur_var env sigma id concl) false hyp0 in
let dep = dep_in_hyps || dep_in_concl in
@@ -4212,7 +4219,7 @@ let msg_not_right_number_induction_arguments scheme =
must be given, so we help a bit the unifier by making the "pattern"
by hand before calling induction_tac *)
let induction_without_atomization isrec with_evars elim names lid =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma, (indsign,scheme) = get_elim_signature elim (List.hd lid) gl in
let nargs_indarg_farg =
scheme.nargs + (if scheme.farg_in_concl then 1 else 0) in
@@ -4247,7 +4254,7 @@ let induction_without_atomization isrec with_evars elim names lid =
(* assume that no occurrences are selected *)
let clear_unselected_context id inhyps cls =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (Tacmach.New.pf_concl gl) &&
cls.concl_occs == NoOccurrences
then user_err
@@ -4493,7 +4500,7 @@ let induction_destruct isrec with_evars (lc,elim) =
match lc with
| [] -> assert false (* ensured by syntax, but if called inside caml? *)
| [c,(eqname,names as allnames),cls] ->
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
match elim with
@@ -4594,8 +4601,8 @@ let simple_destruct = function
*)
let elim_scheme_type elim t =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let clause = Tacmach.New.of_old (fun gl -> mk_clenv_type_of gl elim) gl in
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let clause = mk_clenv_type_of gl elim in
match EConstr.kind clause.evd (last_arg clause.evd clause.templval.rebus) with
| Meta mv ->
let clause' =
@@ -4634,7 +4641,7 @@ let case_type t =
let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make ()
let maybe_betadeltaiota_concl allowred gl =
- let concl = Tacmach.New.pf_nf_concl gl in
+ let concl = Tacmach.New.pf_concl gl in
let sigma = Tacmach.New.project gl in
if not allowred then concl
else
@@ -4891,7 +4898,7 @@ let abstract_subproof id gk tac =
let open Tacticals.New in
let open Tacmach.New in
let open Proofview.Notations in
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let current_sign = Global.named_context_val ()
and global_sign = Proofview.Goal.hyps gl in
@@ -4980,7 +4987,7 @@ let tclABSTRACT name_op tac =
abstract_subproof s gk tac
let unify ?(state=full_transparent_state) x y =
- Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
try
let core_flags =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0087d607d..67e29cf56 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -29,7 +29,7 @@ open Locus
(** {6 General functions. } *)
-val is_quantified_hypothesis : Id.t -> ([`NF],'b) Proofview.Goal.t -> bool
+val is_quantified_hypothesis : Id.t -> ('a, 'r) Proofview.Goal.t -> bool
(** {6 Primitive tactics. } *)
@@ -75,7 +75,7 @@ val intros : unit Proofview.tactic
(** [depth_of_quantified_hypothesis b h g] returns the index of [h] in
the conclusion of goal [g], up to head-reduction if [b] is [true] *)
val depth_of_quantified_hypothesis :
- bool -> quantified_hypothesis -> ([`NF],'b) Proofview.Goal.t -> int
+ bool -> quantified_hypothesis -> ('a, 'r) Proofview.Goal.t -> int
val intros_until : quantified_hypothesis -> unit Proofview.tactic
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index f343cc73d..e90d8a4fd 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -364,8 +364,8 @@ 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 p) gl in
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
let sigma = Tacmach.New.project gl in
let u,v = destruct_ind sigma type_of_pq
in let lb_type_of_p =
@@ -574,12 +574,10 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
in
let fresh_id s gl =
- Tacmach.New.of_old begin fun gsig ->
- let fresh = fresh_id (!avoid) s gsig in
+ let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
- end gl
in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -602,7 +600,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Tacticals.New.tclREPEAT (
Tacticals.New.tclTHENLIST [
Simple.apply_in freshz (EConstr.of_constr (andb_prop()));
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let fresht = fresh_id (Id.of_string "Z") gl in
destruct_on_as (EConstr.mkVar freshz)
(IntroOrPattern [[dl,IntroNaming (IntroIdentifier fresht);
@@ -613,7 +611,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Ci a1 ... an = Ci b1 ... bn
replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto
*)
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
match EConstr.kind sigma concl with
@@ -720,12 +718,10 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
( List.map (fun (_,_,_,slb) -> slb) list_id )
in
let fresh_id s gl =
- Tacmach.New.of_old begin fun gsig ->
- let fresh = fresh_id (!avoid) s gsig in
+ let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
- end gl
in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -748,7 +744,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro()));
simplest_split ;Auto.default_auto ]
);
- Proofview.Goal.nf_enter { enter = begin fun gls ->
+ Proofview.Goal.enter { enter = begin fun gls ->
let concl = Proofview.Goal.concl gls in
let sigma = Tacmach.New.project gl in
(* assume the goal to be eq (eq_type ...) = true *)
@@ -869,12 +865,10 @@ let compute_dec_tact ind lnamesparrec nparrec =
( List.map (fun (_,_,_,slb) -> slb) list_id )
in
let fresh_id s gl =
- Tacmach.New.of_old begin fun gsig ->
- let fresh = fresh_id (!avoid) s gsig in
+ let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in
avoid := fresh::(!avoid); fresh
- end gl
in
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -905,7 +899,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
))
(Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto);
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let freshH2 = fresh_id (Id.of_string "H") gl in
Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [
(* left *)
@@ -917,7 +911,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
;
(*right *)
- Proofview.Goal.nf_enter { enter = begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let freshH3 = fresh_id (Id.of_string "H") gl in
Tacticals.New.tclTHENLIST [
simplest_right ;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 09:28:59 +0000