aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-10-20 13:04:45 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-10-20 14:05:54 +0200
commitcc42541eeaaec0371940e07efdb009a4ee74e468 (patch)
tree6c8d5f3986551cd87027c3417a091b20a97f0f08 /tactics
parentf5d8d305c34f9bab21436c765aeeb56a65005dfe (diff)
Boxing the Goal.enter primitive into a record type.
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml41
-rw-r--r--tactics/autorewrite.ml8
-rw-r--r--tactics/class_tactics.ml15
-rw-r--r--tactics/contradiction.ml16
-rw-r--r--tactics/eauto.ml430
-rw-r--r--tactics/elim.ml16
-rw-r--r--tactics/eqdecide.ml21
-rw-r--r--tactics/equality.ml92
-rw-r--r--tactics/extratactics.ml444
-rw-r--r--tactics/inv.ml22
-rw-r--r--tactics/leminv.ml5
-rw-r--r--tactics/rewrite.ml17
-rw-r--r--tactics/tacinterp.ml116
-rw-r--r--tactics/tacticals.ml53
-rw-r--r--tactics/tactics.ml244
-rw-r--r--tactics/tauto.ml45
16 files changed, 376 insertions, 369 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 686d4b471..4e4eafe4e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -96,11 +96,11 @@ 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 begin fun gl ->
+ Proofview.Goal.nf_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
Clenvtac.clenv_refine false clenv
- end
+ end }
let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
@@ -151,11 +151,12 @@ let conclPattern concl pat tac =
with Constr_matching.PatternMatchingFailure ->
Tacticals.New.tclZEROMSG (str "conclPattern")
in
- Proofview.Goal.enter (fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
constr_bindings env sigma >>= fun constr_bindings ->
- Hook.get forward_interp_tactic constr_bindings tac)
+ Hook.get forward_interp_tactic constr_bindings tac
+ end }
(***********************************************************)
(** A debugging / verbosity framework for trivial and auto *)
@@ -320,7 +321,7 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
let rec trivial_fail_db dbg mod_delta db_list local_db =
let intro_tac =
Tacticals.New.tclTHEN (dbg_intro dbg)
- ( Proofview.Goal.enter begin fun gl ->
+ ( Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let nf c = Evarutil.nf_evar sigma c in
@@ -329,15 +330,15 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
let hintl = make_resolve_hyp env sigma hyp
in trivial_fail_db dbg mod_delta db_list
(Hint_db.add_list env sigma hintl local_db)
- end)
+ end })
in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = Tacmach.New.pf_nf_concl gl in
Tacticals.New.tclFIRST
((dbg_assumption dbg)::intro_tac::
(List.map Tacticals.New.tclCOMPLETE
(trivial_resolve dbg mod_delta db_list local_db concl)))
- end
+ end }
and my_find_search_nodelta db_list local_db hdc concl =
List.map (fun hint -> (None,hint))
@@ -414,7 +415,7 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
"nocore" amongst the databases. *)
let trivial ?(debug=Off) lems dbnames =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let db_list = make_db_list dbnames in
@@ -422,10 +423,10 @@ let trivial ?(debug=Off) lems dbnames =
let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(trivial_fail_db d false db_list hints)
- end
+ end }
let full_trivial ?(debug=Off) lems =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let db_list = current_pure_db () in
@@ -433,7 +434,7 @@ let full_trivial ?(debug=Off) lems =
let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(trivial_fail_db d false db_list hints)
- end
+ end }
let gen_trivial ?(debug=Off) lems = function
| None -> full_trivial ~debug lems
@@ -466,10 +467,10 @@ let extend_local_db decl db gl =
let intro_register dbg kont db =
Tacticals.New.tclTHEN (dbg_intro dbg)
- (Proofview.Goal.enter begin fun gl ->
+ (Proofview.Goal.enter { enter = begin fun gl ->
let extend_local_db decl db = extend_local_db decl db gl in
Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db))
- end)
+ end })
(* n is the max depth of search *)
(* local_db contains the local Hypotheses *)
@@ -482,14 +483,14 @@ let search d n mod_delta db_list local_db =
if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else
Tacticals.New.tclORELSE0 (dbg_assumption d)
(Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
- ( Proofview.Goal.enter begin fun gl ->
+ ( Proofview.Goal.enter { enter = begin fun gl ->
let concl = Tacmach.New.pf_nf_concl gl in
let d' = incr_dbg d in
Tacticals.New.tclFIRST
(List.map
(fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
(possible_resolve d mod_delta db_list local_db concl))
- end))
+ end }))
end []
in
search d n local_db
@@ -497,7 +498,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 begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let db_list = make_db_list dbnames in
@@ -505,7 +506,7 @@ let delta_auto debug mod_delta n lems dbnames =
let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(search d n mod_delta db_list hints)
- end
+ end }
let delta_auto =
if Flags.profile then
@@ -520,7 +521,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 begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let db_list = current_pure_db () in
@@ -528,7 +529,7 @@ let delta_full_auto ?(debug=Off) mod_delta n lems =
let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(search d n mod_delta db_list hints)
- end
+ end }
let full_auto ?(debug=Off) n = delta_full_auto ~debug false n
let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 2ecba176a..43a8d7f06 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -123,7 +123,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
(Proofview.tclUNIT()) lbas))
let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
(* let's check at once if id exists (to raise the appropriate error) *)
let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in
let general_rewrite_in id =
@@ -166,7 +166,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
(List.fold_left (fun tac bas ->
Tacticals.New.tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) (Proofview.tclUNIT()) lbas)))
idl
- end
+ end }
let autorewrite_in ?(conds=Naive) id = autorewrite_multi_in ~conds [id]
@@ -191,10 +191,10 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
| None ->
(* try to rewrite in all hypothesis
(except maybe the rewritten one) *)
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let ids = Tacmach.New.pf_ids_of_hyps gl in
try_do_hyps (fun id -> id) ids
- end)
+ end })
let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds (Proofview.tclUNIT())
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 83b1202b7..9c22beba2 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -140,17 +140,17 @@ let rec eq_constr_mod_evars x y =
| _, _ -> compare_constr eq_constr_mod_evars x y
let progress_evars t =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let check =
- Proofview.Goal.nf_enter begin fun gl' ->
+ Proofview.Goal.nf_enter { enter = begin fun gl' ->
let newconcl = Proofview.Goal.concl gl' in
if eq_constr_mod_evars concl newconcl
then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)")
else Proofview.tclUNIT ()
- end
+ end }
in t <*> check
- end
+ end }
let e_give_exact flags poly (c,clenv) gl =
@@ -188,10 +188,11 @@ let clenv_of_prods poly nprods (c, clenv) gl =
else None
let with_prods nprods poly (c, clenv) f =
- Proofview.Goal.nf_enter (fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
match clenv_of_prods poly nprods (c, clenv) gl with
| None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
- | Some clenv' -> f (c, clenv') gl)
+ | Some clenv' -> f (c, clenv') gl
+ end }
(** Hack to properly solve dependent evars that are typeclasses *)
@@ -901,5 +902,5 @@ let autoapply c i gl =
(Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
let cty = pf_unsafe_type_of gl c in
let ce = mk_clenv_from gl (c,cty) in
- let tac = unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) in
+ let tac = { enter = fun gl -> unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) gl } in
Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 7deb4baf6..34886d74d 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -48,13 +48,13 @@ let filter_hyp f tac =
| [] -> Proofview.tclZERO Not_found
| (id,_,t)::rest when f t -> tac id
| _::rest -> seek rest in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
seek hyps
- end
+ end }
let contradiction_context =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let rec seek_neg l = match l with
@@ -67,11 +67,11 @@ let contradiction_context =
else match kind_of_term typ with
| Prod (na,t,u) when is_empty_type u ->
(Proofview.tclORELSE
- (Proofview.Goal.enter begin fun gl ->
+ (Proofview.Goal.enter { enter = begin fun gl ->
let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
filter_hyp (fun typ -> is_conv_leq typ t)
(fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
- end)
+ end })
begin function (e, info) -> match e with
| Not_found -> seek_neg rest
| e -> Proofview.tclZERO ~info e
@@ -80,7 +80,7 @@ let contradiction_context =
in
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
seek_neg hyps
- end
+ end }
let is_negation_of env sigma typ t =
match kind_of_term (whd_betadeltaiota env sigma t) with
@@ -90,7 +90,7 @@ let is_negation_of env sigma typ t =
| _ -> false
let contradiction_term (c,lbind as cl) =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let type_of = Tacmach.New.pf_unsafe_type_of gl in
@@ -113,7 +113,7 @@ let contradiction_term (c,lbind as cl) =
| Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.")
| e -> Proofview.tclZERO ~info e
end
- end
+ end }
let contradiction = function
| None -> Tacticals.New.tclTHEN intros contradiction_context
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index d0fd4b078..08502e0cc 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -28,26 +28,27 @@ open Misctypes
open Locus
open Locusops
open Hints
+open Proofview.Notations
DECLARE PLUGIN "eauto"
let eauto_unif_flags = auto_flags_of_state full_transparent_state
let e_give_exact ?(flags=eauto_unif_flags) c =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let t1 = Tacmach.New.pf_unsafe_type_of gl c in
let t2 = Tacmach.New.pf_concl gl in
if occur_existential t1 || occur_existential t2 then
Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c))
else exact_check c
- end
+ end }
let assumption id = e_give_exact (mkVar id)
let e_assumption =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl))
- end
+ end }
TACTIC EXTEND eassumption
| [ "eassumption" ] -> [ e_assumption ]
@@ -58,10 +59,10 @@ TACTIC EXTEND eexact
END
let registered_e_assumption =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id))
(Tacmach.New.pf_ids_of_hyps gl))
- end
+ end }
(************************************************************************)
(* PROLOG tactic *)
@@ -126,15 +127,14 @@ open Unification
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 begin
- fun gl ->
+ Proofview.Goal.nf_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)
- end
+ end }
let hintmap_of hdc concl =
match hdc with
@@ -152,19 +152,19 @@ let e_exact poly flags (c,clenv) =
in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c)
let rec e_trivial_fail_db db_list local_db =
- let next = Proofview.Goal.nf_enter begin fun gl ->
+ let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
let d = Tacmach.New.pf_last_hyp gl in
let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) d in
e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) hintl local_db)
- end in
- Proofview.Goal.enter begin fun gl ->
+ end } in
+ Proofview.Goal.enter { enter = begin fun gl ->
let tacl =
registered_e_assumption ::
(Tacticals.New.tclTHEN Tactics.intro next) ::
(List.map fst (e_trivial_resolve db_list local_db (Tacmach.New.pf_nf_concl gl)))
in
Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
- end
+ end }
and e_my_find_search db_list local_db hdc concl =
let hint_of_db = hintmap_of hdc concl in
@@ -567,7 +567,7 @@ let unfold_head env (ids, csts) c =
in aux c
let autounfold_one db cl =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
let st =
@@ -586,7 +586,7 @@ let autounfold_one db cl =
| Some hyp -> change_in_hyp None (make_change_arg c') hyp
| None -> convert_concl_no_check c' DEFAULTcast
else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
- end
+ end }
(* Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *)
(* (Id.Set.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *)
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 4841d2c25..27e96637d 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -84,7 +84,7 @@ let tmphyp_name = Id.of_string "_TmpHyp"
let up_to_delta = ref false (* true *)
let general_decompose recognizer c =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let type_of = pf_unsafe_type_of gl in
let typc = type_of c in
tclTHENS (cut typc)
@@ -93,7 +93,7 @@ let general_decompose recognizer c =
(ifOnHyp recognizer (general_decompose_aux recognizer)
(fun id -> Proofview.V82.tactic (clear [id]))));
Proofview.V82.tactic (exact_no_check c) ]
- end
+ end }
let head_in indl t gl =
let env = Proofview.Goal.env gl in
@@ -107,10 +107,10 @@ let head_in indl t gl =
with Not_found -> false
let decompose_these c l =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let indl = List.map (fun x -> x, Univ.Instance.empty) l in
general_decompose (fun (_,t) -> head_in indl t gl) c
- end
+ end }
let decompose_and c =
general_decompose
@@ -138,7 +138,7 @@ let induction_trailer abs_i abs_j bargs =
(tclDO (abs_j - abs_i) intro)
(onLastHypId
(fun id ->
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let idty = pf_unsafe_type_of gl (mkVar id) in
let fvty = global_vars (pf_env gl) idty in
let possible_bring_hyps =
@@ -156,11 +156,11 @@ let induction_trailer abs_i abs_j bargs =
(tclTHENLIST
[bring_hyps hyps; tclTRY (Proofview.V82.tactic (clear ids));
simple_elimination (mkVar id)])
- end
+ end }
))
let double_ind h1 h2 =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let abs_i = of_old (depth_of_quantified_hypothesis true h1) gl in
let abs_j = of_old (depth_of_quantified_hypothesis true h2) gl in
let abs =
@@ -173,7 +173,7 @@ let double_ind h1 h2 =
(fun id ->
elimination_then
(introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id))))
- end
+ end }
let h_double_induction = double_ind
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 4fb76bb82..74e5e036a 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -27,6 +27,7 @@ open Constr_matching
open Hipattern
open Tacmach.New
open Coqlib
+open Proofview.Notations
(* This file containts the implementation of the tactics ``Decide
Equality'' and ``Compare''. They can be used to decide the
@@ -146,7 +147,7 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
intros_reflexivity;
]
| a1 :: largs, a2 :: rargs ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let rectype = pf_unsafe_type_of gl a1 in
let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
@@ -154,13 +155,13 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
(tclTHENS (elim_type decide) subtacs)
- end
+ end }
| _ -> invalid_arg "List.fold_right2"
let solveEqBranch rectype =
Proofview.tclORELSE
begin
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = pf_nf_concl gl in
match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) ->
let (mib,mip) = Global.lookup_inductive rectype in
@@ -169,7 +170,7 @@ let solveEqBranch rectype =
let rargs = getargs rhs
and largs = getargs lhs in
solveArg [] eqonleft op largs rargs
- end
+ end }
end
begin function (e, info) -> match e with
| PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!")
@@ -185,7 +186,7 @@ let hd_app c = match kind_of_term c with
let decideGralEquality =
Proofview.tclORELSE
begin
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = pf_nf_concl gl in
match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) ->
let headtyp = hd_app (pf_compute gl typ) in
@@ -196,7 +197,7 @@ let decideGralEquality =
(tclTHEN
(mkBranches c1 c2)
(tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
- end
+ end }
end
begin function (e, info) -> match e with
| PatternMatchingFailure ->
@@ -207,20 +208,20 @@ let decideGralEquality =
let decideEqualityGoal = tclTHEN intros decideGralEquality
let decideEquality rectype =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let decide = mkGenDecideEqGoal rectype gl in
(tclTHENS (cut decide) [default_auto;decideEqualityGoal])
- end
+ end }
(* The tactic Compare *)
let compare c1 c2 =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let rectype = pf_unsafe_type_of gl c1 in
let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
(tclTHENS (cut decide)
[(tclTHEN intro
(tclTHEN (onLastHyp simplest_case) clear_last));
decideEquality rectype])
- end
+ end }
diff --git a/tactics/equality.ml b/tactics/equality.ml
index fdc77be2f..e8f88fca1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -207,10 +207,10 @@ let rewrite_conv_closed_unif_flags = {
}
let rewrite_elim with_evars frzevars cls c e =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in
general_elim_clause with_evars flags cls c e
- end
+ end }
(* Ad hoc asymmetric general_elim_clause *)
let general_elim_clause with_evars frzevars cls rew elim =
@@ -245,7 +245,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
(general_elim_clause with_evars frzevars cls c elim))
tac
in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let instantiate_lemma concl =
if not all then instantiate_lemma gl c t l l2r concl
else instantiate_lemma_all frzevars gl c t l l2r concl
@@ -257,7 +257,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
let cs = instantiate_lemma typ in
if firstonly then tclFIRST (List.map try_clause cs)
else tclMAP try_clause cs
- end
+ end }
(* The next function decides in particular whether to try a regular
rewrite or a generalized rewrite.
@@ -383,7 +383,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
if occs != AllOccurrences then (
rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
else
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let ctype = get_type_of env sigma c in
@@ -411,7 +411,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
| None -> Proofview.tclZERO ~info e
(* error "The provided term does not end with an equality or a declared rewrite relation." *)
end
- end
+ end }
let general_rewrite_ebindings =
general_rewrite_ebindings_clause None
@@ -473,9 +473,9 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
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
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
do_hyps_atleastonce (ids gl)
- end
+ end }
in
if cl.concl_occs == NoOccurrences then do_hyps else
tclIFTHENTRYELSEMUST
@@ -483,7 +483,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
do_hyps
let apply_special_clear_request clear_flag f =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
try
@@ -491,17 +491,17 @@ let apply_special_clear_request clear_flag f =
apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
with
e when catchable_exception e -> tclIDTAC
- end
+ end }
let general_multi_rewrite with_evars l cl tac =
let do1 l2r f =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let (c, sigma) = run_delayed env sigma f in
tclWITHHOLES with_evars
(general_rewrite_clause l2r with_evars ?tac c cl) sigma
- end
+ end }
in
let rec doN l2r c = function
| Precisely n when n <= 0 -> Proofview.tclUNIT ()
@@ -564,7 +564,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
| None -> Proofview.tclUNIT ()
| Some tac -> tclCOMPLETE tac
in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let get_type_of = pf_apply get_type_of gl in
let t1 = get_type_of c1
and t2 = get_type_of c2 in
@@ -590,7 +590,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
tclTHEN (apply sym) assumption;
try_prove_eq
])))
- end
+ end }
let replace c1 c2 =
replace_using_leibniz onConcl c2 c1 false false None
@@ -873,7 +873,7 @@ let rec build_discriminator env sigma dirn c sort = function
*)
let gen_absurdity id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
let hyp_typ = pf_nf_evar gl hyp_typ in
if is_empty_type hyp_typ
@@ -881,7 +881,7 @@ let gen_absurdity id =
simplest_elim (mkVar id)
else
tclZEROMSG (str "Not the negation of an equality.")
- end
+ end }
(* Precondition: eq is leibniz equality
@@ -937,7 +937,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
match find_positions env sigma t1 t2 with
@@ -946,10 +946,10 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
| Inl (cpath, (_,dirn), _) ->
let sort = pf_apply get_type_of gl concl in
discr_positions env sigma u eq_clause cpath dirn sort
- end
+ end }
let onEquality with_evars tac (c,lbindc) =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_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
@@ -961,10 +961,10 @@ let onEquality with_evars tac (c,lbindc) =
tclTHEN
(Proofview.Unsafe.tclEVARS eq_clause'.evd)
(tac (eq,eqn,eq_args) eq_clause')
- end
+ end }
let onNegatedEquality with_evars tac =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let ccl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
@@ -975,7 +975,7 @@ let onNegatedEquality with_evars tac =
onEquality with_evars tac (mkVar id,NoBindings)))
| _ ->
tclZEROMSG (str "Not a negated primitive equality.")
- end
+ end }
let discrSimpleClause with_evars = function
| None -> onNegatedEquality with_evars discrEq
@@ -1244,7 +1244,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 begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
try
let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
(* fetch the informations of the pair *)
@@ -1282,7 +1282,7 @@ let inject_if_homogenous_dependent_pair ty =
])]
with Exit ->
Proofview.tclUNIT ()
- end
+ end }
(* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it
expands then only when the whdnf has a constructor of an inductive type
@@ -1374,7 +1374,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 begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let sort = pf_apply get_type_of gl (Proofview.Goal.concl gl) in
let sigma = clause.evd in
let env = Proofview.Goal.env gl in
@@ -1386,7 +1386,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
| Inr posns ->
inject_at_positions env sigma true u clause posns
(ntac (clenv_value clause))
- end
+ end }
let dEqThen with_evars ntac = function
| None -> onNegatedEquality with_evars (decompEqThen (ntac None))
@@ -1397,10 +1397,10 @@ let dEq with_evars =
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
let intro_decompe_eq tac data cl =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let cl = pf_apply make_clenv_binding gl cl NoBindings in
decompEqThen (fun _ -> tac) data cl
- end
+ end }
let _ = declare_intro_decomp_eq intro_decompe_eq
@@ -1500,7 +1500,7 @@ let cutSubstInConcl l2r eqn =
end }
let cutSubstInHyp l2r eqn id =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
let typ = pf_get_hyp_typ id gl in
let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
@@ -1512,7 +1512,7 @@ let cutSubstInHyp l2r eqn id =
(replace_core (onHyp id) l2r eqn)
])
(change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly))
- end
+ end }
let try_rewrite tac =
Proofview.tclORELSE tac begin function (e, info) -> match e with
@@ -1534,11 +1534,11 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
let substClause l2r c cls =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let eq = pf_apply get_type_of gl c in
tclTHENS (cutSubstClause l2r eq cls)
[Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)]
- end
+ end }
let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
let rewriteInHyp l2r c id = rewriteClause l2r c (Some id)
@@ -1564,7 +1564,7 @@ user = raise user error specific to rewrite
(* Substitutions tactics (JCF) *)
let unfold_body x =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
(** We normalize the given hypothesis immediately. *)
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
let (_, xval, _) = Context.lookup_named x hyps in
@@ -1581,7 +1581,7 @@ let unfold_body x =
let reductc = Proofview.V82.tactic (fun gl -> reduct_in_concl (rfun, DEFAULTcast) gl) in
tclTHENLIST [tclMAP reducth hl; reductc]
end
- end
+ end }
let restrict_to_eq_and_identity eq = (* compatibility *)
if not (is_global glob_eq eq) &&
@@ -1604,7 +1604,7 @@ let is_eq_x gl x (id,_,c) =
erase hyp and x; proceed by generalizing all dep hyps *)
let subst_one dep_proof_ok x (hyp,rhs,dir) =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
@@ -1630,13 +1630,13 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
else
[Proofview.tclUNIT ()]) @
[tclTRY (clear [x; hyp])])
- end
+ end }
(* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite
it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *)
let subst_one_var dep_proof_ok x =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.assume gl in
let (_,xval,_) = pf_get_hyp x gl in
(* If x has a body, simply replace x with body and clear x *)
@@ -1655,7 +1655,7 @@ let subst_one_var dep_proof_ok x =
str".")
with FoundHyp res -> res in
subst_one dep_proof_ok x res
- end
+ end }
let subst_gen dep_proof_ok ids =
tclTHEN Proofview.V82.nf_evar_goals (tclMAP (subst_one_var dep_proof_ok) ids)
@@ -1715,7 +1715,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
(* Second step: treat equations *)
let process hyp =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.assume gl in
let find_eq_data_decompose = find_eq_data_decompose gl in
let (_,_,c) = pf_get_hyp hyp gl in
@@ -1729,19 +1729,19 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
| _ ->
Proofview.tclUNIT ()
- end
+ end }
in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let ids = find_equations gl in
tclMAP process ids
- end
+ end }
else
(* 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 begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let find_eq_data_decompose = find_eq_data_decompose gl in
let test (_,c) =
try
@@ -1758,7 +1758,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
let ids = List.map_filter test hyps in
let ids = List.uniquize ids in
subst_gen flags.rewrite_dependent_proof ids
- end
+ end }
(* Rewrite the first assumption for which a condition holds
and gives the direction of the rewrite *)
@@ -1794,10 +1794,10 @@ let rewrite_assumption_cond cond_eq_term cl =
with | Failure _ | UserError _ -> arec rest gl
end
in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
arec hyps gl
- end
+ end }
(* Generalize "subst x" to substitution of subterm appearing as an
equation in the context, but not clearing the hypothesis *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 7b754636f..fa13234a6 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -22,6 +22,7 @@ open Evd
open Equality
open Misctypes
open Sigma.Notations
+open Proofview.Notations
DECLARE PLUGIN "extratactics"
@@ -346,7 +347,7 @@ END
(* Refine *)
let refine_tac {Glob_term.closure=closure;term=term} =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let flags = Pretyping.all_no_fail_flags in
@@ -362,7 +363,7 @@ let refine_tac {Glob_term.closure=closure;term=term} =
Sigma.Unsafe.of_pair (c, sigma)
end } in
Tactics.New.refine ~unsafe:false update
- end
+ end }
TACTIC EXTEND refine
[ "refine" uconstr(c) ] -> [ refine_tac c ]
@@ -662,7 +663,7 @@ END
*)
let hget_evar n =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
let evl = evar_list concl in
@@ -672,7 +673,7 @@ let hget_evar n =
let ev = List.nth evl (n-1) in
let ev_type = existential_type sigma ev in
change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
- end
+ end }
TACTIC EXTEND hget_evar
| [ "hget_evar" int_or_var(n) ] -> [ hget_evar (out_arg n) ]
@@ -691,12 +692,12 @@ END
exception Found of unit Proofview.tactic
let rewrite_except h =
- Proofview.Goal.nf_enter begin fun gl ->
+ 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))
hyps
- end
+ end }
let refl_equal =
@@ -710,27 +711,27 @@ 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 begin fun gl ->
+ 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
Tacticals.New.tclTHENLIST
[Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
change_concl
(snd (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl))
- end;
+ end };
simplest_case a]
- end
+ end }
let case_eq_intros_rewrite x =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let n = nb_prod (Proofview.Goal.concl gl) in
(* Pp.msgnl (Printer.pr_lconstr x); *)
Tacticals.New.tclTHENLIST [
mkCaseEq x;
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_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 concl in
@@ -739,9 +740,9 @@ let case_eq_intros_rewrite x =
Tacticals.New.tclDO (n'-n-1) intro;
introduction h;
rewrite_except h]
- end
+ end }
]
- end
+ end }
let rec find_a_destructable_match t =
match kind_of_term t with
@@ -761,15 +762,15 @@ let destauto t =
with Found tac -> tac
let destauto_in id =
- Proofview.Goal.nf_enter begin fun gl ->
+ 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
(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
(* Pp.msgnl (Printer.pr_lconstr (ctype)); *)
destauto ctype
- end
+ end }
TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Proofview.Goal.nf_enter (fun gl -> destauto (Proofview.Goal.concl gl)) ]
+| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ]
| [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
END
@@ -777,10 +778,11 @@ END
(* ********************************************************************* *)
let eq_constr x y =
- Proofview.Goal.enter (fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let evd = Proofview.Goal.sigma gl in
if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT ()
- else Tacticals.New.tclFAIL 0 (str "Not equal"))
+ else Tacticals.New.tclFAIL 0 (str "Not equal")
+ end }
TACTIC EXTEND constr_eq
| [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ]
@@ -981,14 +983,14 @@ TACTIC EXTEND guard
END
let decompose l c =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let to_ind c =
if isInd c then Univ.out_punivs (destInd c)
else error "not an inductive type"
in
let l = List.map to_ind l in
Elim.h_decompose l c
- end
+ end }
TACTIC EXTEND decompose
| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ]
diff --git a/tactics/inv.ml b/tactics/inv.ml
index f326e2479..a9fa52e92 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -270,14 +270,14 @@ Nota: with Inversion_clear, only four useless hypotheses
let generalizeRewriteIntros as_mode tac depids id =
Proofview.tclENV >>= fun env ->
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_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
[bring_hyps dids; tac;
(* may actually fail to replace if dependent in a previous eq *)
reintros (ids_of_named_context dids)])
- end
+ end }
let error_too_many_names pats =
let loc = Loc.join_loc (fst (List.hd pats)) (fst (List.last pats)) in
@@ -339,7 +339,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 begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
(** 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
let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in
@@ -347,7 +347,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
| Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1
| _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2
| _ -> tac id
- end
+ end }
in
let deq_trailer id clear_flag _ neqns =
assert (clear_flag == None);
@@ -374,7 +374,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
id
let nLastDecls i tac =
- Proofview.Goal.nf_enter (fun gl -> tac (nLastDecls gl i))
+ Proofview.Goal.nf_enter { enter = begin fun gl -> tac (nLastDecls gl i) end }
(* Introduction of the equations on arguments
othin: discriminates Simple Inversion, Inversion and Inversion_clear
@@ -382,7 +382,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 begin fun gl ->
+ Proofview.Goal.nf_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 pi1 nodepids else [] in
@@ -415,7 +415,7 @@ let rewrite_equations as_mode othin neqns names ba =
[tclDO neqns intro;
bring_hyps nodepids;
clear (ids_of_named_context nodepids)])
- end
+ end }
let interp_inversion_kind = function
| SimpleInversion -> None
@@ -514,12 +514,12 @@ 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 begin fun gl ->
+ Proofview.Goal.nf_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 nb_prod_init = nb_prod concl in
let intros_replace_ids =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = pf_nf_concl gl in
let nb_of_new_hyp =
nb_prod concl - (List.length hyps + nb_prod_init)
@@ -528,7 +528,7 @@ let invIn k names ids id =
intros_replacing ids
else
tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids)
- end
+ end }
in
Proofview.tclORELSE
(tclTHENLIST
@@ -536,7 +536,7 @@ let invIn k names ids id =
inversion k NoDep names id;
intros_replace_ids])
(wrap_inv_error id)
- end
+ end }
let invIn_gen k names idl = try_intros_until (invIn k names idl)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 42d22bc3c..04a78dc57 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -27,6 +27,7 @@ open Declare
open Tacticals.New
open Tactics
open Decl_kinds
+open Proofview.Notations
let no_inductive_inconstr env sigma constr =
(str "Cannot recognize an inductive predicate in " ++
@@ -268,7 +269,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 begin fun gl ->
+ Proofview.Goal.nf_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
@@ -280,7 +281,7 @@ let lemInvIn id c ids =
in
((tclTHEN (tclTHEN (bring_hyps hyps) (Proofview.V82.tactic (lemInv id c)))
(intros_replace_ids)))
- end
+ end }
let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 7e0182137..2667fa7ff 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -35,6 +35,7 @@ open Environ
open Termops
open Libnames
open Sigma.Notations
+open Proofview.Notations
(** Typeclass-based generalized rewriting. *)
@@ -1501,7 +1502,7 @@ let rec insert_dependent env decl accu hyps = match hyps with
insert_dependent env decl (ndecl :: accu) rem
let assert_replacing id newt tac =
- let prf = Proofview.Goal.nf_enter begin fun gl ->
+ let prf = Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let ctx = Environ.named_context env in
@@ -1518,7 +1519,7 @@ let assert_replacing id newt tac =
let (e, _) = destEvar ev in
Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q)
end }
- end in
+ end } in
Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
let newfail n s =
@@ -1544,14 +1545,14 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
convert_hyp_no_check (id, None, newt)
| None, Some p ->
Proofview.Unsafe.tclEVARS undef <*>
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let make = { run = begin fun sigma ->
let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in
Sigma (mkApp (p, [| ev |]), sigma, q)
end } in
Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
- end
+ end }
| None, None ->
Proofview.Unsafe.tclEVARS undef <*>
convert_concl_no_check newt DEFAULTcast
@@ -1562,7 +1563,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
| None -> Proofview.tclUNIT ()
| Some id -> Proofview.V82.tactic (Tactics.reduct_in_hyp beta_red (id, InHyp))
in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
@@ -1590,7 +1591,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
with
| PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) ->
raise (RewriteFailure (Himsg.explain_pretype_error env evd e))
- end
+ end }
let tactic_init_setoid () =
try init_setoid (); tclIDTAC
@@ -2037,7 +2038,7 @@ let not_declared env ty rel =
str ty ++ str" relation. Maybe you need to require the Setoid library")
let setoid_proof ty fn fallback =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
@@ -2066,7 +2067,7 @@ let setoid_proof ty fn fallback =
| e' -> Proofview.tclZERO ~info e'
end
end
- end
+ end }
let tac_open ((evm,_), c) tac =
Proofview.V82.tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 895064951..1ea19bce0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -632,10 +632,10 @@ let pf_interp_constr ist gl =
let new_interp_constr ist c k =
let open Proofview in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k c)
- end
+ end }
let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
let try_expand_ltac_var sigma x =
@@ -1172,9 +1172,9 @@ 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 begin fun gl -> Tactics.tclABSTRACT
+ Proofview.Goal.nf_enter { enter = begin fun gl -> Tactics.tclABSTRACT
(Option.map (Tacmach.New.of_old (pf_interp_ident ist) gl) ido) (interp_tactic ist tac)
- end
+ end }
| TacThen (t1,t) ->
Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t)
| TacDispatch tl ->
@@ -1350,7 +1350,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacML (loc,opn,l) ->
let trace = push_trace (loc,LtacMLCall tac) ist in
let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let goal_sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
@@ -1364,7 +1364,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let name () = Pptactic.pr_tactic env (TacML(loc,opn,args)) in
Proofview.Trace.name_tactic name
(catch_error_tac trace (tac args ist))
- end
+ end }
and force_vrec ist v : typed_generic_argument Ftactic.t =
let v = Value.normalize v in
@@ -1803,7 +1803,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
match tac with
(* Basic tactics *)
| TacIntroPattern l ->
- Proofview.Goal.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,l' = interp_intro_pattern_list_as_list ist env sigma l in
@@ -1813,9 +1813,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* spiwack: print uninterpreted, not sure if it is the
expected behaviour. *)
(Tactics.intros_patterns l')) sigma
- end
+ end }
| TacIntroMove (ido,hto) ->
- Proofview.Goal.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 mloc = interp_move_location ist env sigma hto in
@@ -1823,7 +1823,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
name_atomic ~env
(TacIntroMove(ido,mloc))
(Tactics.intro_move ido mloc)
- end
+ end }
| TacExact c ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin
@@ -1838,7 +1838,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacApply (a,ev,cb,cl) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin
- Proofview.Goal.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 l = List.map (fun (k,c) ->
@@ -1851,10 +1851,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in
sigma, Tactics.apply_delayed_in a ev clear id l cl in
Tacticals.New.tclWITHHOLES ev tac sigma
- end
+ end }
end
| TacElim (ev,(keep,cb),cbo) ->
- Proofview.Goal.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, cb = interp_constr_with_bindings ist env sigma cb in
@@ -1864,9 +1864,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac
in
Tacticals.New.tclWITHHOLES ev named_tac sigma
- end
+ end }
| TacCase (ev,(keep,cb)) ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
@@ -1875,16 +1875,16 @@ and interp_atomic ist tac : unit Proofview.tactic =
name_atomic ~env (TacCase(ev,(keep,cb))) tac
in
Tacticals.New.tclWITHHOLES ev named_tac sigma
- end
+ end }
| TacFix (idopt,n) ->
- Proofview.Goal.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 idopt = Option.map (interp_ident ist env sigma) idopt in
name_atomic ~env
(TacFix(idopt,n))
(Proofview.V82.tactic (Tactics.fix idopt n))
- end
+ end }
| TacMutualFix (id,n,l) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin
@@ -1903,14 +1903,14 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
end
| TacCofix idopt ->
- Proofview.Goal.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 idopt = Option.map (interp_ident ist env sigma) idopt in
name_atomic ~env
(TacCofix (idopt))
(Proofview.V82.tactic (Tactics.cofix idopt))
- end
+ end }
| TacMutualCofix (id,l) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin
@@ -1929,7 +1929,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
end
| TacAssert (b,t,ipat,c) ->
- Proofview.Goal.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,c) =
@@ -1941,9 +1941,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
(name_atomic ~env
(TacAssert(b,t,ipat,c))
(Tactics.forward b tac ipat' c)) sigma
- end
+ end }
| TacGeneralize cl ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
@@ -1951,7 +1951,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(name_atomic ~env
(TacGeneralize cl)
(Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma
- end
+ end }
| TacGeneralizeDep c ->
(new_interp_constr ist c) (fun c ->
name_atomic (* spiwack: probably needs a goal environment *)
@@ -1960,7 +1960,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
)
| TacLetTac (na,c,clp,b,eqpat) ->
Proofview.V82.nf_evar_goals <*>
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let clp = interp_clause ist env sigma clp in
@@ -1993,7 +1993,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
(let_pat_tac b (interp_name ist env sigma na)
((sigma,sigma'),c) clp eqpat) sigma')
- end
+ end }
(* Automation tactics *)
| TacTrivial (debug,lems,l) ->
@@ -2003,7 +2003,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
++strbrk"does not print traces anymore." ++ spc()
++strbrk"Use \"Info 1 trivial\", instead.")
end;
- Proofview.Goal.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 lems = interp_auto_lemmas ist env sigma lems in
@@ -2012,7 +2012,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(Auto.h_trivial ~debug
lems
(Option.map (List.map (interp_hint_base ist)) l))
- end
+ end }
| TacAuto (debug,n,lems,l) ->
begin if debug == Tacexpr.Info then
msg_warning
@@ -2020,7 +2020,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
++strbrk"does not print traces anymore." ++ spc()
++strbrk"Use \"Info 1 auto\", instead.")
end;
- Proofview.Goal.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 lems = interp_auto_lemmas ist env sigma lems in
@@ -2029,14 +2029,14 @@ and interp_atomic ist tac : unit Proofview.tactic =
(Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
lems
(Option.map (List.map (interp_hint_base ist)) l))
- end
+ end }
(* Derived basic tactics *)
| 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_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sigma,l =
@@ -2060,7 +2060,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(Tacticals.New.tclTHEN
(Proofview.Unsafe.tclEVARS sigma)
(Tactics.induction_destruct isrec ev (l,el)))
- end
+ end }
| TacDoubleInduction (h1,h2) ->
let h1 = interp_quantified_hypothesis ist h1 in
let h2 = interp_quantified_hypothesis ist h2 in
@@ -2069,7 +2069,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(Elim.h_double_induction h1 h2)
(* Context management *)
| TacClear (b,l) ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Tacmach.New.pf_env gl in
let sigma = Proofview.Goal.sigma gl in
let l = interp_hyp_list ist env sigma l in
@@ -2078,16 +2078,16 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* spiwack: until the tactic is in the monad *)
let tac = Proofview.V82.tactic (fun gl -> Tactics.clear l gl) in
Proofview.Trace.name_tactic (fun () -> Pp.str"<clear>") tac
- end
+ end }
| TacClearBody l ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Tacmach.New.pf_env gl in
let sigma = Proofview.Goal.sigma gl in
let l = interp_hyp_list ist env sigma l in
name_atomic ~env
(TacClearBody l)
(Tactics.clear_body l)
- end
+ end }
| TacMove (id1,id2) ->
Proofview.V82.tactic begin fun gl ->
Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1)
@@ -2095,7 +2095,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
gl
end
| TacRename l ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Tacmach.New.pf_env gl in
let sigma = Proofview.Goal.sigma gl in
let l =
@@ -2106,11 +2106,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
name_atomic ~env
(TacRename l)
(Tactics.rename_hyp l)
- end
+ end }
(* Constructors *)
| TacSplit (ev,bll) ->
- Proofview.Goal.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, bll = List.fold_map (interp_bindings ist env) sigma bll in
@@ -2119,7 +2119,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
name_atomic ~env (TacSplit (ev, bll)) tac
in
Tacticals.New.tclWITHHOLES ev named_tac sigma
- end
+ end }
(* Conversion *)
| TacReduce (r,cl) ->
(* spiwack: until the tactic is in the monad *)
@@ -2163,7 +2163,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* 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 begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
Proofview.V82.tactic begin fun gl ->
@@ -2182,23 +2182,23 @@ and interp_atomic ist tac : unit Proofview.tactic =
(Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
{ gl with sigma = sigma }
end
- end
+ end }
end
(* Equivalence relations *)
| TacSymmetry c ->
- Proofview.Goal.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 cl = interp_clause ist env sigma c in
name_atomic ~env
(TacSymmetry cl)
(Tactics.intros_symmetry cl)
- end
+ end }
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let l' = List.map (fun (b,m,(keep,c)) ->
let f = { delayed = fun env sigma ->
let sigma = Sigma.to_evar_map sigma in
@@ -2215,9 +2215,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
(Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by),
Equality.Naive)
by))
- end
+ end }
| TacInversion (DepInversion (k,c,ids),hyp) ->
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (sigma,c_interp) =
@@ -2235,9 +2235,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
(name_atomic ~env
(TacInversion(DepInversion(k,c_interp,ids),dqhyps))
(Inv.dinv k c_interp ids_interp dqhyps)) sigma
- end
+ end }
| TacInversion (NonDepInversion (k,idl,ids),hyp) ->
- Proofview.Goal.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 hyps = interp_hyp_list ist env sigma idl in
@@ -2247,9 +2247,9 @@ and interp_atomic ist tac : unit Proofview.tactic =
(name_atomic ~env
(TacInversion (NonDepInversion (k,hyps,ids),dqhyps))
(Inv.inv_clause k ids_interp hyps dqhyps)) sigma
- end
+ end }
| TacInversion (InversionUsing (c,idl),hyp) ->
- Proofview.Goal.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,c_interp) = interp_constr ist env sigma c in
@@ -2259,7 +2259,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
name_atomic ~env
(TacInversion (InversionUsing (c_interp,hyps),dqhyps))
(Leminv.lemInv_clause dqhyps c_interp hyps)
- end
+ end }
(* Initial call for interpretation *)
@@ -2280,7 +2280,7 @@ let eval_tactic_ist ist t =
let interp_tac_gen lfun avoid_ids debug t =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let extra = TacStore.set TacStore.empty f_debug debug in
let extra = TacStore.set extra f_avoid_ids avoid_ids in
@@ -2289,7 +2289,7 @@ let interp_tac_gen lfun avoid_ids debug t =
interp_tactic ist
(intern_pure_tactic {
ltacvars; genv = env } t)
- end
+ end }
let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
let _ = Proof_global.set_interp_tac interp
@@ -2309,9 +2309,9 @@ let hide_interp global t ot =
Proofview.tclENV >>= fun env ->
hide_interp env
else
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
hide_interp (Proofview.Goal.env gl)
- end
+ end }
(***************************************************************************)
(** Register standard arguments *)
@@ -2411,7 +2411,7 @@ let _ = Hook.set Auto.extern_interp
let dummy_id = Id.of_string "_"
let lift_constr_tac_to_ml_tac vars tac =
- let tac _ ist = Proofview.Goal.enter begin fun gl ->
+ let tac _ ist = Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let map = function
@@ -2424,5 +2424,5 @@ let lift_constr_tac_to_ml_tac vars tac =
in
let args = List.map_filter map vars in
tac args ist
- end in
+ end } in
tac
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bc82e9ef4..3c56bbdc0 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -538,66 +538,65 @@ module New = struct
mkVar (nthHypId m gl)
let onNthHypId m tac =
- Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end
+ Proofview.Goal.enter { enter = begin fun gl -> tac (nthHypId m gl) end }
let onNthHyp m tac =
- Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end
+ Proofview.Goal.enter { enter = begin fun gl -> tac (nthHyp m gl) end }
let onLastHypId = onNthHypId 1
let onLastHyp = onNthHyp 1
let onNthDecl m tac =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
Proofview.tclUNIT (nthDecl m gl) >>= tac
- end
+ end }
let onLastDecl = onNthDecl 1
let ifOnHyp pred tac1 tac2 id =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let typ = Tacmach.New.pf_get_hyp_typ id gl in
if pred (id,typ) then
tac1 id
else
tac2 id
- end
+ end }
- let onHyps find tac = Proofview.Goal.nf_enter (fun gl -> tac (find gl))
+ let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find gl) end }
let afterHyp id tac =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
let rem, _ = List.split_when (fun (hyp,_,_) -> Id.equal hyp id) hyps in
tac rem
- end
+ end }
let fullGoal gl =
let hyps = Tacmach.New.pf_ids_of_hyps gl in
None :: List.map Option.make hyps
let tryAllHyps tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let hyps = Tacmach.New.pf_ids_of_hyps gl in
tclFIRST_PROGRESS_ON tac hyps
- end
+ end }
let tryAllHypsAndConcl tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
tclFIRST_PROGRESS_ON tac (fullGoal gl)
- end
+ end }
let onClause tac cl =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let hyps = Tacmach.New.pf_ids_of_hyps gl in
tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
- end
+ end }
(* Find the right elimination suffix corresponding to the sort of the goal *)
(* 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
- begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (Proofview.Goal.nf_enter begin fun gl ->
+ (Proofview.Goal.nf_enter { enter = begin fun gl ->
let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
(* applying elimination_scheme just a little modified *)
let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
@@ -649,10 +648,10 @@ module New = struct
Proofview.tclTHEN
(Clenvtac.clenv_refine false clenv')
(Proofview.tclEXTEND [] tclIDTAC branchtacs)
- end) end
+ end }) end }
let elimination_then tac c =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_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
@@ -660,7 +659,7 @@ module New = struct
| Some _ -> false,gl_make_case_dep
in
general_elim_then_using mkelim isrec None tac None ind (c, t)
- end
+ end }
let case_then_using =
general_elim_then_using gl_make_case_dep false
@@ -669,16 +668,16 @@ module New = struct
general_elim_then_using gl_make_case_nodep false
let elim_on_ba tac ba =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in
tac branches
- end
+ end }
let case_on_ba tac ba =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in
tac branches
- end
+ end }
let elimination_sort_of_goal gl =
(** Retyping will expand evars anyway. *)
@@ -695,11 +694,11 @@ module New = struct
| Some id -> elimination_sort_of_hyp id gl
let pf_constr_of_global ref tac =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (sigma, c) = Evd.fresh_global env sigma ref in
Proofview.Unsafe.tclEVARS sigma <*> (tac c)
- end
+ end }
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d3cf154c9..66053a314 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -184,7 +184,7 @@ let unsafe_intro env store (id, c, t) b =
end }
let introduction ?(check=true) id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.assume gl in
let concl = Proofview.Goal.concl gl in
let sigma = Proofview.Goal.sigma gl in
@@ -199,12 +199,12 @@ let introduction ?(check=true) id =
| Prod (_, t, b) -> unsafe_intro env store (id, None, t) b
| LetIn (_, c, t, b) -> unsafe_intro env store (id, Some c, t) b
| _ -> raise (RefinerError IntroNeedsProduct)
- end
+ end }
let refine = Tacmach.refine
let convert_concl ?(check=true) ty k =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let store = Proofview.Goal.extra gl in
let conclty = Proofview.Goal.raw_concl gl in
@@ -221,10 +221,10 @@ let convert_concl ?(check=true) ty k =
let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
Sigma (ans, sigma, p +> q)
end }
- end
+ end }
let convert_hyp ?(check=true) d =
- Proofview.Goal.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 ty = Proofview.Goal.raw_concl gl in
@@ -234,20 +234,20 @@ let convert_hyp ?(check=true) d =
Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true ~store ty
end }
- end
+ end }
let convert_concl_no_check = convert_concl ~check:false
let convert_hyp_no_check = convert_hyp ~check:false
let convert_gen pb x y =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
try
let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in
Proofview.Unsafe.tclEVARS sigma
with (* Reduction.NotConvertible *) _ ->
(** FIXME: Sometimes an anomaly is raised from conversion *)
Tacticals.New.tclFAIL 0 (str "Not convertible")
-end
+end }
let convert x y = convert_gen Reduction.CONV x y
let convert_leq x y = convert_gen Reduction.CUMUL x y
@@ -319,7 +319,7 @@ let rename_hyp repl =
match dom with
| None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping")
| Some (src, dst) ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.assume gl in
let hyps = Proofview.Goal.hyps gl in
let concl = Proofview.Goal.concl gl in
@@ -356,7 +356,7 @@ let rename_hyp repl =
let (sigma, c) = Evarutil.new_evar_instance nctx sigma nconcl ~store instance in
Sigma.Unsafe.of_pair (c, sigma)
end }
- end
+ end }
(**************************************************************)
(* Fresh names *)
@@ -417,7 +417,7 @@ let find_name mayrepl decl naming gl = match naming with
(**************************************************************)
let assert_before_then_gen b naming t tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let id = find_name b (Anonymous,None,t) naming gl in
Tacticals.New.tclTHENLAST
(Proofview.V82.tactic
@@ -426,7 +426,7 @@ let assert_before_then_gen b naming t tac =
with Evarutil.ClearDependencyError (id,err) ->
error_replacing_dependency (pf_env gl) (project gl) id err))
(tac id)
- end
+ end }
let assert_before_gen b naming t =
assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ())
@@ -435,7 +435,7 @@ let assert_before na = assert_before_gen false (naming_of_name na)
let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id))
let assert_after_then_gen b naming t tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let id = find_name b (Anonymous,None,t) naming gl in
Tacticals.New.tclTHENFIRST
(Proofview.V82.tactic
@@ -444,7 +444,7 @@ let assert_after_then_gen b naming t tac =
with Evarutil.ClearDependencyError (id,err) ->
error_replacing_dependency (pf_env gl) (project gl) id err))
(tac id)
- end
+ end }
let assert_after_gen b naming t =
assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ()))
@@ -783,7 +783,7 @@ let build_intro_tac id dest tac = match dest with
Proofview.V82.tactic (move_hyp id dest); tac id]
let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
let concl = nf_evar (Proofview.Goal.sigma gl) concl in
match kind_of_term concl with
@@ -809,7 +809,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
| e -> Proofview.tclZERO ~info e
end
- end
+ end }
let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ())
let intro_mustbe_force id = intro_gen (NamingMustBe (dloc,id)) MoveLast true false
@@ -873,14 +873,14 @@ let get_previous_hyp_position id gl =
aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
let intro_replacing id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let next_hyp = get_next_hyp_position id gl in
Tacticals.New.tclTHENLIST [
Proofview.V82.tactic (thin_for_replacing [id]);
introduction id;
Proofview.V82.tactic (move_hyp id next_hyp);
]
- end
+ end }
(* We have e.g. [x, y, y', x', y'' |- forall y y' y'', G] and want to
reintroduce y, y,' y''. Note that we have to clear y, y' and y''
@@ -892,7 +892,7 @@ let intro_replacing id =
(* the behavior of inversion *)
let intros_possibly_replacing ids =
let suboptimal = true in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
Tacticals.New.tclTHEN
(Tacticals.New.tclMAP (fun id ->
@@ -901,16 +901,16 @@ let intros_possibly_replacing ids =
(Tacticals.New.tclMAP (fun (id,pos) ->
Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id))
posl)
- end
+ end }
(* This version assumes that replacement is actually possible *)
let intros_replacing ids =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let posl = List.map (fun id -> (id, get_next_hyp_position id gl)) ids in
Tacticals.New.tclTHEN
(Proofview.V82.tactic (thin_for_replacing ids))
(Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl)
- end
+ end }
(* User-level introduction tactics *)
@@ -954,10 +954,10 @@ let depth_of_quantified_hypothesis red h gl =
str".")
let intros_until_gen red h =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let n = Tacmach.New.of_old (depth_of_quantified_hypothesis red h) gl in
Tacticals.New.tclDO n (if red then introf else intro)
- end
+ end }
let intros_until_id id = intros_until_gen false (NamedHyp id)
let intros_until_n_gen red n = intros_until_gen red (AnonHyp n)
@@ -998,20 +998,20 @@ let onOpenInductionArg env sigma tac = function
(intros_until_n n)
(Tacticals.New.onLastHyp
(fun c ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let pending = (sigma,sigma) in
tac clear_flag (pending,(c,NoBindings))
- end))
+ end }))
| clear_flag,ElimOnIdent (_,id) ->
(* A quantified hypothesis *)
Tacticals.New.tclTHEN
(try_intros_until_id_check id)
- (Proofview.Goal.enter begin fun gl ->
+ (Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let pending = (sigma,sigma) in
tac clear_flag (pending,(mkVar id,NoBindings))
- end)
+ end })
let onInductionArg tac = function
| clear_flag,ElimOnConstr cbl ->
@@ -1036,7 +1036,7 @@ let map_induction_arg f = function
(****************************************)
let cut c =
- Proofview.Goal.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 concl = Tacmach.New.pf_nf_concl gl in
@@ -1062,7 +1062,7 @@ let cut c =
end }
else
Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
- end
+ end }
let error_uninstantiated_metas t clenv =
let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
@@ -1171,12 +1171,12 @@ let enforce_prop_bound_names rename tac =
mkLetIn (na,c,t,aux (push_rel (na,Some c,t) env) sigma (i-1) t')
| _ -> print_int i; Pp.msg (print_constr t); assert false in
let rename_branch i =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let t = Proofview.Goal.concl gl in
change_concl (aux env sigma i t)
- end in
+ end } in
(if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
tac
(Array.map rename_branch nn)
@@ -1191,7 +1191,7 @@ let rec contract_letin_in_lam_header c =
let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ())
rename i (elim, elimty, bindings) indclause =
- Proofview.Goal.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 elim = contract_letin_in_lam_header elim in
@@ -1204,7 +1204,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
in
let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags)
- end
+ end }
(*
* Elimination tactic with bindings and using an arbitrary
@@ -1221,7 +1221,7 @@ type eliminator = {
}
let general_elim_clause_gen elimtac indclause elim =
- Proofview.Goal.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 (elimc,lbindelimc) = elim.elimbody in
@@ -1229,10 +1229,10 @@ let general_elim_clause_gen elimtac indclause elim =
let i =
match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause
- end
+ end }
let general_elim with_evars clear_flag (c, lbindc) elim =
- Proofview.Goal.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 ct = Retyping.get_type_of env sigma c in
@@ -1242,7 +1242,7 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
Tacticals.New.tclTHEN
(general_elim_clause_gen elimtac indclause elim)
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
- end
+ end }
(* Case analysis tactics *)
@@ -1349,7 +1349,7 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
id rename i (elim, elimty, bindings) indclause =
- Proofview.Goal.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 elim = contract_letin_in_lam_header elim in
@@ -1372,7 +1372,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
(str "Nothing to rewrite in " ++ pr_id id ++ str".");
clenv_refine_in with_evars id id sigma elimclause''
(fun id -> Proofview.tclUNIT ())
- end
+ end }
let general_elim_clause with_evars flags id c e =
let elim = match id with
@@ -1427,7 +1427,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 begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
try
@@ -1448,7 +1448,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
NotADefinedRecordUseScheme (snd elim) in
Tacticals.New.tclFIRST
(List.init n (fun i ->
- Proofview.Goal.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
match make_projection env sigma params cstr sign elim i n c u with
@@ -1459,10 +1459,10 @@ let descend_in_conjunctions avoid tac (err, info) c =
[Proofview.V82.tactic (refine p);
(* Might be ill-typed due to forbidden elimination. *)
Tacticals.New.onLastHypId (tac (not isrec))]
- end))
+ end }))
| None -> Proofview.tclZERO ~info err
with RefinerError _|UserError _ -> Proofview.tclZERO ~info err
- end
+ end }
(****************************************************)
(* Resolution tactics *)
@@ -1495,7 +1495,7 @@ let tclORELSEOPT t k =
| Some tac -> tac)
let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let flags =
if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
@@ -1504,7 +1504,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
step. *)
let concl_nprod = nb_prod concl in
let rec try_main_apply with_destruct c =
- Proofview.Goal.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
@@ -1558,14 +1558,14 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
| PretypeError _|RefinerError _|UserError _|Failure _ ->
Some (try_red_apply thm_ty0 (e, info))
| _ -> None)
- end
+ end }
in
Tacticals.New.tclTHENLIST [
try_main_apply with_destruct c;
solve_remaining_apply_goals;
apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
]
- end
+ end }
let rec apply_with_bindings_gen b e = function
| [] -> Proofview.tclUNIT ()
@@ -1577,13 +1577,13 @@ let rec apply_with_bindings_gen b e = function
let apply_with_delayed_bindings_gen b e l =
let one k (loc, f) =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let (cb, sigma) = run_delayed env sigma f in
Tacticals.New.tclWITHHOLES e
(general_apply b b e k (loc,cb)) sigma
- end
+ end }
in
let rec aux = function
| [] -> Proofview.tclUNIT ()
@@ -1646,7 +1646,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 =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let flags =
@@ -1655,7 +1655,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
let targetid = find_name true (Anonymous,None,t') naming gl in
let rec aux idstoclear with_destruct c =
- Proofview.Goal.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
try
@@ -1672,14 +1672,14 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
(descend_in_conjunctions [targetid]
(fun b id -> aux (id::idstoclear) b (mkVar id))
(e, info) c)
- end
+ end }
in
aux [] with_destruct d
- end
+ end }
let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming
id (clear_flag,(loc,f)) tac =
- Proofview.Goal.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 (c, sigma) = run_delayed env sigma f in
@@ -1687,7 +1687,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
(apply_in_once sidecond_first with_delta with_destruct with_evars
naming id (clear_flag,(loc,c)) tac)
sigma
- end
+ end }
(* A useful resolution tactic which, if c:A->B, transforms |- C into
|- B -> C and |- A
@@ -1707,7 +1707,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
*)
let cut_and_apply c =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
| Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
let concl = Proofview.Goal.concl gl in
@@ -1720,7 +1720,7 @@ let cut_and_apply c =
Sigma (ans, sigma, p +> q)
end }
| _ -> error "lapply needs a non-dependent product."
- end
+ end }
(********************************************************************)
(* Exact tactics *)
@@ -1780,10 +1780,10 @@ let assumption =
Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar id) h }
else arec gl only_eq rest
in
- let assumption_tac gl =
+ let assumption_tac = { enter = begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
arec gl true hyps
- in
+ end } in
Proofview.Goal.nf_enter assumption_tac
(*****************************************************************)
@@ -1826,7 +1826,7 @@ let check_decl env (_, c, ty) msg =
msg e
let clear_body ids =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
let ctx = named_context env in
@@ -1862,7 +1862,7 @@ let clear_body ids =
Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
Evarutil.new_evar env sigma concl
end }
- end
+ end }
let clear_wildcards ids =
Proofview.V82.tactic (tclMAP (fun (loc,id) gl ->
@@ -1922,7 +1922,7 @@ let specialize (c,lbind) g =
(* Keeping only a few hypotheses *)
let keep hyps =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
Proofview.tclENV >>= fun env ->
let ccl = Proofview.Goal.concl gl in
let cl,_ =
@@ -1935,7 +1935,7 @@ let keep hyps =
~init:([],[]) (Proofview.Goal.env gl)
in
Proofview.V82.tactic (fun gl -> thin cl gl)
- end
+ end }
(************************)
(* Introduction tactics *)
@@ -1991,7 +1991,7 @@ let rec tclANY tac = function
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 begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let cl = Tacmach.New.pf_nf_concl gl in
let reduce_to_quantified_ind =
Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
@@ -2001,7 +2001,7 @@ let any_constructor with_evars tacopt =
Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
if Int.equal nconstr 0 then error "The type has no constructors.";
tclANY tac (List.interval 1 nconstr)
- end
+ end }
let left_with_bindings with_evars = constructor_tac with_evars (Some 2) 1
let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2
@@ -2052,7 +2052,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 begin fun gl ->
+ Proofview.Goal.nf_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
@@ -2063,10 +2063,10 @@ let intro_decomp_eq loc l thin tac id =
(eq,t,eq_args) (c, t)
| None ->
Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
- end
+ end }
let intro_or_and_pattern loc bracketed ll thin tac id =
- Proofview.Goal.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 ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
@@ -2077,7 +2077,7 @@ let intro_or_and_pattern loc bracketed ll thin tac id =
(Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id])))
(Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
nv (Array.of_list ll))
- end
+ end }
let rewrite_hyp assert_style l2r id =
let rew_on l2r =
@@ -2085,7 +2085,7 @@ let rewrite_hyp assert_style l2r id =
let subst_on l2r x rhs =
Hook.get forward_subst_one true x (id,rhs,l2r) in
let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let type_of = Tacmach.New.pf_unsafe_type_of gl in
let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
@@ -2107,7 +2107,7 @@ let rewrite_hyp assert_style l2r id =
Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id]))
| _ ->
Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (clear [id]))
- end
+ end }
let rec prepare_naming loc = function
| IntroIdentifier id -> NamingMustBe (loc,id)
@@ -2243,7 +2243,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
Proofview.tclUNIT () (* apply_in_once do a replacement *)
else
Proofview.V82.tactic (clear [id]) in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let (c, sigma) = run_delayed env sigma f in
@@ -2255,7 +2255,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
(fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id)))
(tac thin None []))
sigma
- end
+ end }
and prepare_intros_loc loc dft destopt = function
| IntroNaming ipat ->
@@ -2318,7 +2318,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
let tac (naming,lemma) tac id =
apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
naming id lemma tac in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let destopt =
if with_evars then MoveLast (* evars would depend on the whole context *)
else get_previous_hyp_position id gl in
@@ -2329,7 +2329,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
in
(* We chain apply_in_once, ending with an intro pattern *)
List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
- end
+ end }
(*
if sidecond_first then
@@ -2477,12 +2477,12 @@ let letin_pat_tac with_eq id c occs =
let forward b usetac ipat c =
match usetac with
| None ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let t = Tacmach.New.pf_unsafe_type_of gl c in
let hd = head_ident c in
Tacticals.New.tclTHENFIRST (assert_as true hd ipat t)
(Proofview.V82.tactic (exact_no_check c))
- end
+ end }
| Some tac ->
if b then
Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac
@@ -2512,7 +2512,7 @@ let apply_type hdcty argl gl =
let bring_hyps hyps =
if List.is_empty hyps then Tacticals.New.tclIDTAC
else
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let concl = Tacmach.New.pf_nf_concl gl in
let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
@@ -2521,14 +2521,14 @@ let bring_hyps hyps =
let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma newcl in
Sigma (mkApp (ev, args), sigma, p)
end }
- end
+ end }
let revert hyps =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.assume gl in
let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in
(bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps))
- end
+ end }
(* Compute a name for a generalization *)
@@ -2809,7 +2809,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
match ra with
| (RecArg,deprec,recvarname) ::
(IndArg,depind,hyprecname) :: ra' ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let (recpat,names) = match names with
| [loc,IntroNaming (IntroIdentifier id) as pat] ->
let id' = next_ident_away (add_prefix "IH" id) avoid in
@@ -2817,37 +2817,37 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
| _ -> consume_pattern avoid (Name recvarname) deprec gl names in
let dest = get_recarg_dest dests in
dest_intro_patterns avoid thin dest [recpat] (fun ids thin ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let (hyprec,names) =
consume_pattern avoid (Name hyprecname) depind gl names
in
dest_intro_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
peel_tac ra' (update_dest dests ids') names thin)
- end)
- end
+ end })
+ end }
| (IndArg,dep,hyprecname) :: ra' ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
let pat,names =
consume_pattern avoid (Name hyprecname) dep gl names in
dest_intro_patterns avoid thin MoveLast [pat] (fun ids thin ->
peel_tac ra' (update_dest dests ids) names thin)
- end
+ end }
| (RecArg,dep,recvarname) :: ra' ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let (pat,names) =
consume_pattern avoid (Name recvarname) dep gl names in
let dest = get_recarg_dest dests in
dest_intro_patterns avoid thin dest [pat] (fun ids thin ->
peel_tac ra' dests names thin)
- end
+ end }
| (OtherArg,dep,_) :: ra' ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let (pat,names) = consume_pattern avoid Anonymous dep gl names in
let dest = get_recarg_dest dests in
safe_dest_intro_patterns avoid thin dest [pat] (fun ids thin ->
peel_tac ra' dests names thin)
- end
+ end }
| [] ->
check_unused_names names;
Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests)
@@ -2861,7 +2861,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
(* Marche pas... faut prendre en compte l'occurrence précise... *)
let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in
let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in
@@ -2910,7 +2910,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
(atomize_one (i-1) (mkVar x::args) (x::avoid))
in
atomize_one (List.length argl) [] []
- end
+ end }
(* [cook_sign] builds the lists [beforetoclear] (preceding the
ind. var.) and [aftertoclear] (coming after the ind. var.) of hyps
@@ -3362,7 +3362,7 @@ let abstract_args gl generalize_vars dep id defined f args =
else None
let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
Coqlib.check_required_library Coqlib.jmeq_module_name;
let (f, args, def, id, oldid) =
let oldid = Tacmach.New.pf_get_new_id id gl in
@@ -3394,7 +3394,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
[revert vars ;
Proofview.V82.tactic (fun gl -> tclMAP (fun id ->
tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)])
- end
+ end }
let rec compare_upto_variables x y =
if (isVar x || isRel x) && (isVar y || isRel y) then true
@@ -3817,12 +3817,12 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac =
end }
let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in
atomize_param_of_ind_then elim_info hyp0 (fun indvars ->
apply_induction_in_context (Some hyp0) inhyps (pi3 elim_info) indvars names
(fun elim -> Proofview.V82.tactic (induction_tac with_evars [] [hyp0] elim)))
- end
+ end }
let msg_not_right_number_induction_arguments scheme =
str"Not the right number of induction arguments (expected " ++
@@ -3839,7 +3839,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 begin fun gl ->
+ Proofview.Goal.nf_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
@@ -3870,7 +3870,7 @@ let induction_without_atomization isrec with_evars elim names lid =
]) in
let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in
apply_induction_in_context None [] elim indvars names induct_tac
- end
+ end }
(* assume that no occurrences are selected *)
let clear_unselected_context id inhyps cls gl =
@@ -4021,7 +4021,7 @@ let induction_gen clear_flag isrec with_evars elim
let inhyps = match cls with
| Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps
| _ -> [] in
- Proofview.Goal.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 ccl = Proofview.Goal.raw_concl gl in
@@ -4057,7 +4057,7 @@ let induction_gen clear_flag isrec with_evars elim
isrec with_evars info_arg elim id arg t inhyps cls
(induction_with_atomization_of_ind_arg
isrec with_evars elim names id inhyps)
- end
+ end }
(* Induction on a list of arguments. First make induction arguments
atomic (using letins), then do induction. The specificity here is
@@ -4082,7 +4082,7 @@ let induction_gen_l isrec with_evars elim names lc =
atomize_list l'
| _ ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let type_of = Tacmach.New.pf_unsafe_type_of gl in
let x =
id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
@@ -4093,7 +4093,7 @@ let induction_gen_l isrec with_evars elim names lc =
Tacticals.New.tclTHEN
(letin_tac None (Name id) c None allHypsAndConcl)
(atomize_list newl')
- end in
+ end } in
Tacticals.New.tclTHENLIST
[
(atomize_list lc);
@@ -4110,7 +4110,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 begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
match elim with
@@ -4135,9 +4135,9 @@ let induction_destruct isrec with_evars (lc,elim) =
(* standard induction *)
onOpenInductionArg env sigma
(fun clear_flag c -> induction_gen clear_flag isrec with_evars elim (c,allnames) cls) c
- end
+ end }
| _ ->
- Proofview.Goal.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
match elim with
@@ -4153,12 +4153,12 @@ let induction_destruct isrec with_evars (lc,elim) =
(onOpenInductionArg env sigma (fun clear_flag a ->
induction_gen clear_flag isrec with_evars None (a,b) cl) a)
(Tacticals.New.tclMAP (fun (a,b,cl) ->
- Proofview.Goal.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
onOpenInductionArg env sigma (fun clear_flag a ->
induction_gen clear_flag false with_evars None (a,b) cl) a
- end) l)
+ end }) l)
| Some elim ->
(* Several induction hyps with induction scheme *)
let finish_evar_resolution f =
@@ -4186,7 +4186,7 @@ let induction_destruct isrec with_evars (lc,elim) =
error "'as' clause with multiple arguments and 'using' clause can only occur last.";
let newlc = List.map (fun (x,_) -> (x,None)) newlc in
induction_gen_l isrec with_evars elim names newlc
- end
+ end }
let induction ev clr c l e =
induction_gen clr true ev e
@@ -4228,7 +4228,7 @@ let simple_destruct = function
*)
let elim_scheme_type elim t =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
let clause = Tacmach.New.of_old (fun gl -> mk_clenv_type_of gl elim) gl in
match kind_of_term (last_arg clause.templval.rebus) with
| Meta mv ->
@@ -4238,7 +4238,7 @@ let elim_scheme_type elim t =
(clenv_meta_type clause mv) clause in
Clenvtac.res_pf clause' ~flags:(elim_flags ()) ~with_evars:false
| _ -> anomaly (Pp.str "elim_scheme_type")
- end
+ end }
let elim_type t =
Proofview.Goal.s_enter { s_enter = begin fun gl sigma ->
@@ -4274,7 +4274,7 @@ let maybe_betadeltaiota_concl allowred gl =
whd_betadeltaiota env sigma concl
let reflexivity_red allowred =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
(* PL: usual reflexivity don't perform any reduction when searching
for an equality, but we may need to do some when called back from
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
@@ -4282,7 +4282,7 @@ let reflexivity_red allowred =
match match_with_equality_type concl with
| None -> Proofview.tclZERO NoEquationFound
| Some _ -> one_constructor 1 NoBindings
- end
+ end }
let reflexivity =
Proofview.tclORELSE
@@ -4324,7 +4324,7 @@ let match_with_equation c =
Proofview.tclZERO NoEquationFound
let symmetry_red allowred =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
(* PL: usual symmetry don't perform any reduction when searching
for an equality, but we may need to do some when called back from
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
@@ -4336,7 +4336,7 @@ let symmetry_red allowred =
(convert_concl_no_check concl DEFAULTcast)
(Tacticals.New.pf_constr_of_global eq_data.sym apply)
| None,eq,eq_kind -> prove_symmetry eq eq_kind
- end
+ end }
let symmetry =
Proofview.tclORELSE
@@ -4350,7 +4350,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
let symmetry_in id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
let sign,t = decompose_prod_assum ctype in
Proofview.tclORELSE
@@ -4368,7 +4368,7 @@ let symmetry_in id =
| NoEquationFound -> Hook.get forward_setoid_symmetry_in id
| e -> Proofview.tclZERO ~info e
end
- end
+ end }
let intros_symmetry =
Tacticals.New.onClause
@@ -4393,7 +4393,7 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make ()
(* This is probably not very useful any longer *)
let prove_transitivity hdcncl eq_kind t =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let (eq1,eq2) = match eq_kind with
| MonomorphicLeibnizEq (c1,c2) ->
mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |])
@@ -4413,10 +4413,10 @@ let prove_transitivity hdcncl eq_kind t =
[ Tacticals.New.tclDO 2 intro;
Tacticals.New.onLastHyp simplest_case;
assumption ]))
- end
+ end }
let transitivity_red allowred t =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
(* PL: usual transitivity don't perform any reduction when searching
for an equality, but we may need to do some when called back from
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
@@ -4433,7 +4433,7 @@ let transitivity_red allowred t =
match t with
| None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
| Some t -> prove_transitivity eq eq_kind t
- end
+ end }
let transitivity_gen t =
Proofview.tclORELSE
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 59c579237..9bee7ab3e 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -18,6 +18,7 @@ open Tacinterp
open Tactics
open Errors
open Util
+open Proofview.Notations
DECLARE PLUGIN "tauto"
@@ -305,13 +306,13 @@ let reduction_not_iff _ist =
let t_reduction_not_iff = tacticIn reduction_not_iff
let intuition_gen ist flags tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.enter { enter = begin fun gl ->
let tac = Value.of_closure ist tac in
let env = Proofview.Goal.env gl in
let vars, ist, intuition = tauto_intuit flags t_reduction_not_iff tac in
let glb_intuition = Tacintern.glob_tactic_env vars env intuition in
eval_tactic_ist ist glb_intuition
- end
+ end }
let tauto_intuitionistic flags =
Proofview.tclORELSE
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 10:56:52 +0000