aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-02 15:38:20 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-02 15:38:20 +0000
commitea879916e09cd19287c831152d7ae2a84c61f4b0 (patch)
treeba48057f7a5aa3fe160ba26313c5a74ec7a96162
parent07df7994675427b353004da666c23ae79444b0e5 (diff)
More Proofview.Goal.enter.
Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad. This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics. This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17000 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--plugins/btauto/refl_btauto.ml70
-rw-r--r--plugins/cc/cctac.ml184
-rw-r--r--plugins/omega/coq_omega.ml246
-rw-r--r--plugins/quote/quote.ml22
-rw-r--r--plugins/setoid_ring/newring.ml444
-rw-r--r--proofs/proofview.ml15
-rw-r--r--proofs/proofview.mli18
-rw-r--r--tactics/auto.ml30
-rw-r--r--tactics/class_tactics.ml18
-rw-r--r--tactics/contradiction.ml80
-rw-r--r--tactics/eqdecide.ml444
-rw-r--r--tactics/equality.ml115
-rw-r--r--tactics/evar_tactics.ml12
-rw-r--r--tactics/extratactics.ml412
-rw-r--r--tactics/inv.ml118
-rw-r--r--tactics/leminv.ml24
-rw-r--r--tactics/rewrite.ml58
-rw-r--r--tactics/tacinterp.ml217
-rw-r--r--tactics/tacticals.ml30
-rw-r--r--tactics/tactics.ml274
-rw-r--r--toplevel/auto_ind_decl.ml62
21 files changed, 928 insertions, 765 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 440309284..8232604f7 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -217,41 +217,45 @@ module Btauto = struct
Tacticals.tclFAIL 0 msg gl
let try_unification env =
- Proofview.Goal.concl >>= fun concl ->
- let eq = Lazy.force eq in
- let t = decomp_term concl in
- match t with
- | Term.App (c, [|typ; p; _|]) when c === eq ->
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ let eq = Lazy.force eq in
+ let t = decomp_term concl in
+ match t with
+ | Term.App (c, [|typ; p; _|]) when c === eq ->
(* should be an equality [@eq poly ?p (Cst false)] *)
- let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in
- tac
- | _ ->
- let msg = str "Btauto: Internal error" in
- Tacticals.New.tclFAIL 0 msg
+ let tac = Tacticals.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in
+ tac
+ | _ ->
+ let msg = str "Btauto: Internal error" in
+ Tacticals.New.tclFAIL 0 msg
+ end
let tac =
- Proofview.Goal.concl >>= fun concl ->
- let eq = Lazy.force eq in
- let bool = Lazy.force Bool.typ in
- let t = decomp_term concl in
- match t with
- | Term.App (c, [|typ; tl; tr|])
- when typ === bool && c === eq ->
- let env = Env.empty () in
- let fl = Bool.quote env tl in
- let fr = Bool.quote env tr in
- let env = Env.to_list env in
- let fl = reify env fl in
- let fr = reify env fr in
- let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
- Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (Tactics.change_in_concl None changed_gl);
- Proofview.V82.tactic (Tactics.apply (Lazy.force soundness));
- Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
- try_unification env
- ]
- | _ ->
- let msg = str "Cannot recognize a boolean equality" in
- Tacticals.New.tclFAIL 0 msg
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ let eq = Lazy.force eq in
+ let bool = Lazy.force Bool.typ in
+ let t = decomp_term concl in
+ match t with
+ | Term.App (c, [|typ; tl; tr|])
+ when typ === bool && c === eq ->
+ let env = Env.empty () in
+ let fl = Bool.quote env tl in
+ let fr = Bool.quote env tr in
+ let env = Env.to_list env in
+ let fl = reify env fl in
+ let fr = reify env fr in
+ let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
+ Tacticals.New.tclTHENLIST [
+ Proofview.V82.tactic (Tactics.change_in_concl None changed_gl);
+ Proofview.V82.tactic (Tactics.apply (Lazy.force soundness));
+ Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
+ try_unification env
+ ]
+ | _ ->
+ let msg = str "Cannot recognize a boolean equality" in
+ Tacticals.New.tclFAIL 0 msg
+ end
end
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index c12dd4799..dee57cd04 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -348,25 +348,27 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
simplest_elim false_t]
let discriminate_tac cstr p =
- let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
- Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) >>= fun intype ->
- Proofview.Goal.concl >>= fun concl ->
- let outsort = mkType (Termops.new_univ ()) in
- Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>= fun xid ->
- Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) >>= fun tid ->
- let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
- Tacmach.New.of_old (fun gls -> pf_type_of gls identity) >>= fun trivial ->
- let outtype = mkType (Termops.new_univ ()) in
- let pred=mkLambda(Name xid,outtype,mkRel 1) in
- Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>= fun hid ->
- Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) >>= fun proj ->
- let injt=mkApp (Lazy.force _f_equal,
- [|intype;outtype;proj;t1;t2;mkVar hid|]) in
- let endt=mkApp (Lazy.force _eq_rect,
- [|outtype;trivial;pred;identity;concl;injt|]) in
- let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
+ Proofview.Goal.enter begin fun gl ->
+ let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
+ Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) >>= fun intype ->
+ let concl = Proofview.Goal.concl gl in
+ let outsort = mkType (Termops.new_univ ()) in
+ Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) >>= fun xid ->
+ Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) >>= fun tid ->
+ let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
+ Tacmach.New.of_old (fun gls -> pf_type_of gls identity) >>= fun trivial ->
+ let outtype = mkType (Termops.new_univ ()) in
+ let pred=mkLambda(Name xid,outtype,mkRel 1) in
+ Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) >>= fun hid ->
+ Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) >>= fun proj ->
+ let injt=mkApp (Lazy.force _f_equal,
+ [|intype;outtype;proj;t1;t2;mkVar hid|]) in
+ let endt=mkApp (Lazy.force _eq_rect,
+ [|outtype;trivial;pred;identity;concl;injt|]) in
+ let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in
Tacticals.New.tclTHENS (assert_tac (Name hid) neweq)
[proof_tac p; Proofview.V82.tactic (exact_check endt)]
+ end
(* wrap everything *)
@@ -378,58 +380,58 @@ let build_term_to_complete uf meta pac =
applistc (mkConstruct cinfo.ci_constr) all_args
let cc_tactic depth additionnal_terms =
- Proofview.tclUNIT () >= fun () -> (* delay for check_required_library *)
- Coqlib.check_required_library Coqlib.logic_module_name;
- let _ = debug (Pp.str "Reading subgoal ...") in
- Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) >>= fun state ->
- let _ = debug (Pp.str "Problem built, solving ...") in
- let sol = execute true state in
- let _ = debug (Pp.str "Computation completed.") in
- let uf=forest state in
+ Proofview.Goal.enter begin fun gl ->
+ Coqlib.check_required_library Coqlib.logic_module_name;
+ let _ = debug (Pp.str "Reading subgoal ...") in
+ Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) >>= fun state ->
+ let _ = debug (Pp.str "Problem built, solving ...") in
+ let sol = execute true state in
+ let _ = debug (Pp.str "Computation completed.") in
+ let uf=forest state in
match sol with
- None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
- | Some reason ->
- debug (Pp.str "Goal solved, generating proof ...");
- match reason with
- Discrimination (i,ipac,j,jpac) ->
- let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
- let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
- discriminate_tac cstr p
- | Incomplete ->
- Proofview.Goal.env >>= fun env ->
- let metacnt = ref 0 in
- let newmeta _ = incr metacnt; _M !metacnt in
- let terms_to_complete =
- List.map
- (build_term_to_complete uf newmeta)
- (epsilons uf) in
- Pp.msg_info
- (Pp.str "Goal is solvable by congruence but \
+ None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
+ | Some reason ->
+ debug (Pp.str "Goal solved, generating proof ...");
+ match reason with
+ Discrimination (i,ipac,j,jpac) ->
+ let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
+ let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
+ discriminate_tac cstr p
+ | Incomplete ->
+ let env = Proofview.Goal.env gl in
+ let metacnt = ref 0 in
+ let newmeta _ = incr metacnt; _M !metacnt in
+ let terms_to_complete =
+ List.map
+ (build_term_to_complete uf newmeta)
+ (epsilons uf) in
+ Pp.msg_info
+ (Pp.str "Goal is solvable by congruence but \
some arguments are missing.");
- Pp.msg_info
- (Pp.str " Try " ++
- hov 8
- begin
- str "\"congruence with (" ++
- prlist_with_sep
- (fun () -> str ")" ++ spc () ++ str "(")
- (Termops.print_constr_env env)
- terms_to_complete ++
- str ")\","
- end ++
- Pp.str " replacing metavariables by arbitrary terms.");
- Tacticals.New.tclFAIL 0 (str "Incomplete")
- | Contradiction dis ->
- let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
- let ta=term uf dis.lhs and tb=term uf dis.rhs in
- match dis.rule with
- Goal -> proof_tac p
- | Hyp id -> refute_tac id ta tb p
- | HeqG id ->
- convert_to_goal_tac id ta tb p
- | HeqnH (ida,idb) ->
- convert_to_hyp_tac ida ta idb tb p
-
+ Pp.msg_info
+ (Pp.str " Try " ++
+ hov 8
+ begin
+ str "\"congruence with (" ++
+ prlist_with_sep
+ (fun () -> str ")" ++ spc () ++ str "(")
+ (Termops.print_constr_env env)
+ terms_to_complete ++
+ str ")\","
+ end ++
+ Pp.str " replacing metavariables by arbitrary terms.");
+ Tacticals.New.tclFAIL 0 (str "Incomplete")
+ | Contradiction dis ->
+ let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
+ let ta=term uf dis.lhs and tb=term uf dis.rhs in
+ match dis.rule with
+ Goal -> proof_tac p
+ | Hyp id -> refute_tac id ta tb p
+ | HeqG id ->
+ convert_to_goal_tac id ta tb p
+ | HeqnH (ida,idb) ->
+ convert_to_hyp_tac ida ta idb tb p
+ end
let cc_fail gls =
errorlabstrm "Congruence" (Pp.str "congruence failed.")
@@ -453,32 +455,34 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal)
*)
let f_equal =
- Proofview.Goal.concl >>= fun concl ->
- Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
- let cut_eq c1 c2 =
- try (* type_of can raise an exception *)
- let ty = Termops.refresh_universes (type_of c1) in
- Proofview.V82.tactic begin
- tclTHENTRY
- (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
- (simple_reflexivity ())
- end
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
- in
- Proofview.tclORELSE
- begin match kind_of_term concl with
- | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) ->
- begin match kind_of_term t, kind_of_term t' with
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+ let cut_eq c1 c2 =
+ try (* type_of can raise an exception *)
+ let ty = Termops.refresh_universes (type_of c1) in
+ Proofview.V82.tactic begin
+ tclTHENTRY
+ (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|])))
+ (simple_reflexivity ())
+ end
+ with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ in
+ Proofview.tclORELSE
+ begin match kind_of_term concl with
+ | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) ->
+ begin match kind_of_term t, kind_of_term t' with
| App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
let rec cuts i =
if i < 0 then Tacticals.New.tclTRY (congruence_tac 1000 [])
else Tacticals.New.tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
in cuts (Array.length v - 1)
| _ -> Proofview.tclUNIT ()
- end
- | _ -> Proofview.tclUNIT ()
- end
- begin function
- | Type_errors.TypeError _ -> Proofview.tclUNIT ()
- | e -> Proofview.tclZERO e
- end
+ end
+ | _ -> Proofview.tclUNIT ()
+ end
+ begin function
+ | Type_errors.TypeError _ -> Proofview.tclUNIT ()
+ | e -> Proofview.tclZERO e
+ end
+ end
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index fbf9334e0..c865639e6 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1647,17 +1647,18 @@ let destructure_hyps =
Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
Tacmach.New.of_old decidability >>= fun decidability ->
Tacmach.New.of_old pf_nf >>= fun pf_nf ->
- let rec loop = function
- | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
- | (i,body,t)::lit ->
- begin try match destructurate_prop t with
+ Proofview.Goal.enter begin fun gl ->
+ let rec loop = function
+ | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
+ | (i,body,t)::lit ->
+ begin try match destructurate_prop t with
| Kapp(False,[]) -> elim_id i
| Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
| Kapp(Or,[t1;t2]) ->
(Tacticals.New.tclTHENS
- (elim_id i)
- [ onClearedName i (fun i -> (loop ((i,None,t1)::lit)));
- onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ])
+ (elim_id i)
+ [ onClearedName i (fun i -> (loop ((i,None,t1)::lit)));
+ onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ])
| Kapp(And,[t1;t2]) ->
Tacticals.New.tclTHEN
(elim_id i)
@@ -1676,7 +1677,7 @@ let destructure_hyps =
let d1 = decidability t1 in
Tacticals.New.tclTHENLIST [
Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp,
- [| t1; t2; d1; mkVar i|])]);
+ [| t1; t2; d1; mkVar i|])]);
(onClearedName i (fun i ->
(loop ((i,None,mk_or (mk_not t1) t2)::lit))))
]
@@ -1684,113 +1685,115 @@ let destructure_hyps =
loop lit
| Kapp(Not,[t]) ->
begin match destructurate_prop t with
- Kapp(Or,[t1;t2]) ->
- Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
- [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
- (onClearedName i (fun i ->
- (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit))))
- ]
- | Kapp(And,[t1;t2]) ->
- let d1 = decidability t1 in
- Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
- [mkApp (Lazy.force coq_not_and,
- [| t1; t2; d1; mkVar i |])]);
- (onClearedName i (fun i ->
- (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
- ]
- | Kapp(Iff,[t1;t2]) ->
- let d1 = decidability t1 in
- let d2 = decidability t2 in
- Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
- [mkApp (Lazy.force coq_not_iff,
- [| t1; t2; d1; d2; mkVar i |])]);
- (onClearedName i (fun i ->
- (loop ((i,None,
- mk_or (mk_and t1 (mk_not t2))
- (mk_and (mk_not t1) t2))::lit))))
- ]
- | Kimp(t1,t2) ->
+ Kapp(Or,[t1;t2]) ->
+ Tacticals.New.tclTHENLIST [
+ Proofview.V82.tactic (generalize_tac
+ [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
+ (onClearedName i (fun i ->
+ (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit))))
+ ]
+ | Kapp(And,[t1;t2]) ->
+ let d1 = decidability t1 in
+ Tacticals.New.tclTHENLIST [
+ Proofview.V82.tactic (generalize_tac
+ [mkApp (Lazy.force coq_not_and,
+ [| t1; t2; d1; mkVar i |])]);
+ (onClearedName i (fun i ->
+ (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
+ ]
+ | Kapp(Iff,[t1;t2]) ->
+ let d1 = decidability t1 in
+ let d2 = decidability t2 in
+ Tacticals.New.tclTHENLIST [
+ Proofview.V82.tactic (generalize_tac
+ [mkApp (Lazy.force coq_not_iff,
+ [| t1; t2; d1; d2; mkVar i |])]);
+ (onClearedName i (fun i ->
+ (loop ((i,None,
+ mk_or (mk_and t1 (mk_not t2))
+ (mk_and (mk_not t1) t2))::lit))))
+ ]
+ | Kimp(t1,t2) ->
(* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok.
For t1, being decidable implies being Prop. *)
- let d1 = decidability t1 in
- Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
- [mkApp (Lazy.force coq_not_imp,
- [| t1; t2; d1; mkVar i |])]);
- (onClearedName i (fun i ->
- (loop ((i,None,mk_and t1 (mk_not t2)) :: lit))))
- ]
- | Kapp(Not,[t]) ->
- let d = decidability t in
- Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
- [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
- (onClearedName i (fun i -> (loop ((i,None,t)::lit))))
- ]
- | Kapp(op,[t1;t2]) ->
- (try
- let thm = not_binop op in
- Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (generalize_tac
- [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
- (onClearedName i (fun _ -> loop lit))
- ]
- with Not_found -> loop lit)
- | Kapp(Eq,[typ;t1;t2]) ->
- if !old_style_flag then begin
- match destructurate_type (pf_nf typ) with
- | Kapp(Nat,_) ->
- Tacticals.New.tclTHENLIST [
- (simplest_elim
- (mkApp
- (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
- (onClearedName i (fun _ -> loop lit))
- ]
- | Kapp(Z,_) ->
- Tacticals.New.tclTHENLIST [
- (simplest_elim
- (mkApp
- (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
- (onClearedName i (fun _ -> loop lit))
- ]
- | _ -> loop lit
- end else begin
- match destructurate_type (pf_nf typ) with
- | Kapp(Nat,_) ->
- (Tacticals.New.tclTHEN
- (Proofview.V82.tactic (convert_hyp_no_check
- (i,body,
- (mkApp (Lazy.force coq_neq, [| t1;t2|])))))
- (loop lit))
- | Kapp(Z,_) ->
- (Tacticals.New.tclTHEN
- (Proofview.V82.tactic (convert_hyp_no_check
- (i,body,
- (mkApp (Lazy.force coq_Zne, [| t1;t2|])))))
- (loop lit))
- | _ -> loop lit
- end
- | _ -> loop lit
+ let d1 = decidability t1 in
+ Tacticals.New.tclTHENLIST [
+ Proofview.V82.tactic (generalize_tac
+ [mkApp (Lazy.force coq_not_imp,
+ [| t1; t2; d1; mkVar i |])]);
+ (onClearedName i (fun i ->
+ (loop ((i,None,mk_and t1 (mk_not t2)) :: lit))))
+ ]
+ | Kapp(Not,[t]) ->
+ let d = decidability t in
+ Tacticals.New.tclTHENLIST [
+ Proofview.V82.tactic (generalize_tac
+ [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
+ (onClearedName i (fun i -> (loop ((i,None,t)::lit))))
+ ]
+ | Kapp(op,[t1;t2]) ->
+ (try
+ let thm = not_binop op in
+ Tacticals.New.tclTHENLIST [
+ Proofview.V82.tactic (generalize_tac
+ [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ with Not_found -> loop lit)
+ | Kapp(Eq,[typ;t1;t2]) ->
+ if !old_style_flag then begin
+ match destructurate_type (pf_nf typ) with
+ | Kapp(Nat,_) ->
+ Tacticals.New.tclTHENLIST [
+ (simplest_elim
+ (mkApp
+ (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | Kapp(Z,_) ->
+ Tacticals.New.tclTHENLIST [
+ (simplest_elim
+ (mkApp
+ (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
+ (onClearedName i (fun _ -> loop lit))
+ ]
+ | _ -> loop lit
+ end else begin
+ match destructurate_type (pf_nf typ) with
+ | Kapp(Nat,_) ->
+ (Tacticals.New.tclTHEN
+ (Proofview.V82.tactic (convert_hyp_no_check
+ (i,body,
+ (mkApp (Lazy.force coq_neq, [| t1;t2|])))))
+ (loop lit))
+ | Kapp(Z,_) ->
+ (Tacticals.New.tclTHEN
+ (Proofview.V82.tactic (convert_hyp_no_check
+ (i,body,
+ (mkApp (Lazy.force coq_Zne, [| t1;t2|])))))
+ (loop lit))
+ | _ -> loop lit
+ end
+ | _ -> loop lit
end
| _ -> loop lit
- with
- | Undecidable -> loop lit
- | e when catchable_exception e -> loop lit
- end
- in
- Proofview.Goal.hyps >>= fun hyps ->
- try (* type_of can raise exceptions *)
- loop (Environ.named_context_of_val hyps)
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ with
+ | Undecidable -> loop lit
+ | e when catchable_exception e -> loop lit
+ end
+ in
+ let hyps = Proofview.Goal.hyps gl in
+ try (* type_of can raise exceptions *)
+ loop (Environ.named_context_of_val hyps)
+ with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
let destructure_goal =
- Proofview.Goal.concl >>= fun concl ->
- Tacmach.New.of_old decidability >>= fun decidability ->
- let rec loop t =
- match destructurate_prop t with
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ Tacmach.New.of_old decidability >>= fun decidability ->
+ let rec loop t =
+ match destructurate_prop t with
| Kapp(Not,[t]) ->
(Tacticals.New.tclTHEN
(Tacticals.New.tclTHEN (Proofview.V82.tactic (unfold sp_not)) intro)
@@ -1798,18 +1801,19 @@ let destructure_goal =
| Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b))
| Kapp(False,[]) -> destructure_hyps
| _ ->
- let goal_tac =
- try
- let dec = decidability t in
- Tacticals.New.tclTHEN
- (Proofview.V82.tactic (Tactics.refine
- (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
- intro
- with Undecidable -> Proofview.V82.tactic (Tactics.elim_type (build_coq_False ()))
- in
- Tacticals.New.tclTHEN goal_tac destructure_hyps
- in
- (loop concl)
+ let goal_tac =
+ try
+ let dec = decidability t in
+ Tacticals.New.tclTHEN
+ (Proofview.V82.tactic (Tactics.refine
+ (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
+ intro
+ with Undecidable -> Proofview.V82.tactic (Tactics.elim_type (build_coq_False ()))
+ in
+ Tacticals.New.tclTHEN goal_tac destructure_hyps
+ in
+ (loop concl)
+ end
let destructure_goal = destructure_goal
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index bf061095c..89d161f73 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -453,18 +453,20 @@ let quote_terms ivs lc =
yet. *)
let quote f lid =
- Tacmach.New.pf_global f >>= fun f ->
- Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>= fun cl ->
- Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs ->
- Proofview.Goal.concl >>= fun concl ->
- Proofview.Goal.lift (quote_terms ivs [concl]) >>= fun quoted_terms ->
- let (p, vm) = match quoted_terms with
- | [p], vm -> (p,vm)
- | _ -> assert false
- in
- match ivs.variable_lhs with
+ Proofview.Goal.enter begin fun gl ->
+ Tacmach.New.pf_global f >>= fun f ->
+ Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_global_sensitive lid) >>= fun cl ->
+ Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs ->
+ let concl = Proofview.Goal.concl gl in
+ Proofview.Goal.lift (quote_terms ivs [concl]) >>= fun quoted_terms ->
+ let (p, vm) = match quoted_terms with
+ | [p], vm -> (p,vm)
+ | _ -> assert false
+ in
+ match ivs.variable_lhs with
| None -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast)
| Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast)
+ end
let gen_quote cont c f lid =
Tacmach.New.pf_global f >>= fun f ->
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 7bd0c7e43..aee7efb76 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -798,16 +798,18 @@ let ltac_ring_structure e =
open Proofview.Notations
let ring_lookup (f:glob_tactic_expr) lH rl t =
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- try (* find_ring_strucure can raise an exception *)
- let rl = make_args_list rl t in
- let e = find_ring_structure env sigma rl in
- let rl = carg (make_term_list e.ring_carrier rl) in
- let lH = carg (make_hyp_list env lH) in
- let ring = ltac_ring_structure e in
- ltac_apply f (ring@[lH;rl])
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ try (* find_ring_strucure can raise an exception *)
+ let rl = make_args_list rl t in
+ let e = find_ring_structure env sigma rl in
+ let rl = carg (make_term_list e.ring_carrier rl) in
+ let lH = carg (make_hyp_list env lH) in
+ let ring = ltac_ring_structure e in
+ ltac_apply f (ring@[lH;rl])
+ with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
TACTIC EXTEND ring_lookup
| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
@@ -1121,16 +1123,18 @@ let ltac_field_structure e =
field_simpl_eq_in_ok;cond_ok;pretac;posttac]
let field_lookup (f:glob_tactic_expr) lH rl t =
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- try
- let rl = make_args_list rl t in
- let e = find_field_structure env sigma rl in
- let rl = carg (make_term_list e.field_carrier rl) in
- let lH = carg (make_hyp_list env lH) in
- let field = ltac_field_structure e in
- ltac_apply f (field@[lH;rl])
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ try
+ let rl = make_args_list rl t in
+ let e = find_field_structure env sigma rl in
+ let rl = carg (make_term_list e.field_carrier rl) in
+ let lH = carg (make_hyp_list env lH) in
+ let field = ltac_field_structure e in
+ ltac_apply f (field@[lH;rl])
+ with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
TACTIC EXTEND field_lookup
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index dace158ac..364cfeb4b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -668,7 +668,12 @@ end
module Goal = struct
- type 'a u = 'a list
+ type t = Environ.env*Evd.evar_map*Environ.named_context_val*Term.constr
+
+ let env (env,_,_,_) = env
+ let sigma (_,sigma,_,_) = sigma
+ let hyps (_,_,hyps,_) = hyps
+ let concl (_,_,_,concl) = concl
let lift s =
(* spiwack: convenience notations, waiting for ocaml 3.12 *)
@@ -688,15 +693,13 @@ module Goal = struct
tclZERO e
let return x = lift (Goal.return x)
- let concl = lift Goal.concl
- let hyps = lift Goal.hyps
- let env = lift Goal.env
+ let enter_t f = Goal.enter (fun env sigma hyps concl -> f (env,sigma,hyps,concl))
let enter f =
- lift (Goal.enter f) >= fun ts ->
+ lift (enter_t f) >= fun ts ->
tclDISPATCH ts
let enterl f =
- lift (Goal.enter f) >= fun ts ->
+ lift (enter_t f) >= fun ts ->
tclDISPATCHL ts >= fun res ->
tclUNIT (List.flatten res)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index fa1a8d56f..6d5e9d75d 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -283,6 +283,13 @@ end
module Goal : sig
+ type t
+
+ val concl : t -> Term.constr
+ val hyps : t -> Environ.named_context_val
+ val env : t -> Environ.env
+ val sigma : t -> Evd.evar_map
+
(* [lift_sensitive s] returns the list corresponding to the evaluation
of [s] on each of the focused goals *)
val lift : 'a Goal.sensitive -> 'a glist tactic
@@ -290,14 +297,9 @@ module Goal : sig
(* [lift (Goal.return x)] *)
val return : 'a -> 'a glist tactic
- val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> unit tactic) -> unit tactic
- val enterl : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> 'a glist tactic) -> 'a glist tactic
- (* [lift Goal.concl] *)
- val concl : Term.constr glist tactic
- (* [lift Goal.hyps] *)
- val hyps : Environ.named_context_val glist tactic
- (* [lift Goal.env] *)
- val env : Environ.env glist tactic
+ val enter : (t -> unit tactic) -> unit tactic
+ val enterl : (t -> 'a glist tactic) -> 'a glist tactic
+
end
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 35b0dc7ff..728eaa3fe 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1275,17 +1275,21 @@ 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.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- Tacmach.New.pf_last_hyp >>= fun hyp ->
- let hintl = make_resolve_hyp env sigma hyp
- in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db))
+ ( Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ Tacmach.New.pf_last_hyp >>= fun hyp ->
+ let hintl = make_resolve_hyp env sigma hyp
+ in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db)
+ end)
in
- Proofview.Goal.concl >>= fun concl ->
- Tacticals.New.tclFIRST
- ((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac::
- (List.map Tacticals.New.tclCOMPLETE
- (trivial_resolve dbg mod_delta db_list local_db concl)))
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ Tacticals.New.tclFIRST
+ ((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac::
+ (List.map Tacticals.New.tclCOMPLETE
+ (trivial_resolve dbg mod_delta db_list local_db concl)))
+ end
and my_find_search_nodelta db_list local_db hdc concl =
List.map (fun hint -> (None,hint))
@@ -1433,12 +1437,14 @@ let search d n mod_delta db_list local_db =
if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
Tacticals.New.tclORELSE0 (Proofview.V82.tactic (dbg_assumption d))
(Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
- ( Proofview.Goal.concl >>= fun concl ->
+ ( Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.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))))
+ (possible_resolve d mod_delta db_list local_db concl))
+ end))
end []
in
search d n local_db
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 1aaf4af00..c33e5fb7c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -83,13 +83,17 @@ let rec eq_constr_mod_evars x y =
| _, _ -> compare_constr eq_constr_mod_evars x y
let progress_evars t =
- Proofview.Goal.concl >>= fun concl ->
- let check =
- Proofview.Goal.concl >>= fun newconcl ->
- if eq_constr_mod_evars concl newconcl
- then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)")
- else Proofview.tclUNIT ()
- in t <*> check
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ let check =
+ Proofview.Goal.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
+ in t <*> check
+ end
let unify_e_resolve flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 74780a8d2..c500a5969 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -44,19 +44,22 @@ let filter_hyp f tac =
| [] -> Proofview.tclZERO Not_found
| (id,_,t)::rest when f t -> tac id
| _::rest -> seek rest in
- Proofview.Goal.hyps >>= fun hyps ->
- seek (Environ.named_context_of_val hyps)
+ Proofview.Goal.enter begin fun gl ->
+ let hyps = Proofview.Goal.hyps gl in
+ seek (Environ.named_context_of_val hyps)
+ end
let contradiction_context =
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- let rec seek_neg l = match l with
- | [] -> Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
- | (id,_,typ)::rest ->
- let typ = whd_betadeltaiota env sigma typ in
- if is_empty_type typ then
- simplest_elim (mkVar id)
- else match kind_of_term typ with
+ Proofview.Goal.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
+ | [] -> Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
+ | (id,_,typ)::rest ->
+ let typ = whd_betadeltaiota env sigma typ in
+ if is_empty_type typ then
+ simplest_elim (mkVar id)
+ else match kind_of_term typ with
| Prod (na,t,u) when is_empty_type u ->
(Proofview.tclORELSE
begin
@@ -69,10 +72,11 @@ let contradiction_context =
| e -> Proofview.tclZERO e
end)
| _ -> seek_neg rest
- in
- Proofview.Goal.hyps >>= fun hyps ->
- let hyps = Environ.named_context_of_val hyps in
- seek_neg hyps
+ in
+ let hyps = Proofview.Goal.hyps gl in
+ let hyps = Environ.named_context_of_val hyps in
+ seek_neg hyps
+ end
let is_negation_of env sigma typ t =
match kind_of_term (whd_betadeltaiota env sigma t) with
@@ -80,28 +84,30 @@ let is_negation_of env sigma typ t =
| _ -> false
let contradiction_term (c,lbind as cl) =
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
- try (* type_of can raise exceptions. *)
- let typ = type_of c in
- let _, ccl = splay_prod env sigma typ in
- if is_empty_type ccl then
- Tacticals.New.tclTHEN (elim false cl None) (Proofview.V82.tactic (tclTRY assumption))
- else
- Proofview.tclORELSE
- begin
- if lbind = NoBindings then
- filter_hyp (is_negation_of env sigma typ)
- (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
- else
- Proofview.tclZERO Not_found
- end
- begin function
- | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
- | e -> Proofview.tclZERO e
- end
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+ try (* type_of can raise exceptions. *)
+ let typ = type_of c in
+ let _, ccl = splay_prod env sigma typ in
+ if is_empty_type ccl then
+ Tacticals.New.tclTHEN (elim false cl None) (Proofview.V82.tactic (tclTRY assumption))
+ else
+ Proofview.tclORELSE
+ begin
+ if lbind = NoBindings then
+ filter_hyp (is_negation_of env sigma typ)
+ (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
+ else
+ Proofview.tclZERO Not_found
+ end
+ begin function
+ | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
+ | e -> Proofview.tclZERO e
+ end
+ with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
let contradiction = function
| None -> Tacticals.New.tclTHEN intros contradiction_context
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 0a6e7a072..a0e8fcb88 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -130,16 +130,18 @@ let solveArg eqonleft op a1 a2 tac =
let solveEqBranch rectype =
Proofview.tclORELSE
begin
- Proofview.Goal.concl >>= fun concl ->
- match_eqdec concl >= fun (eqonleft,op,lhs,rhs,_) ->
- let (mib,mip) = Global.lookup_inductive rectype in
- let nparams = mib.mind_nparams in
- let getargs l = List.skipn nparams (snd (decompose_app l)) in
- let rargs = getargs rhs
- and largs = getargs lhs in
- List.fold_right2
- (solveArg eqonleft op) largs rargs
- (Tacticals.New.tclTHEN (choose_eq eqonleft) h_reflexivity)
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ match_eqdec concl >= fun (eqonleft,op,lhs,rhs,_) ->
+ let (mib,mip) = Global.lookup_inductive rectype in
+ let nparams = mib.mind_nparams in
+ let getargs l = List.skipn nparams (snd (decompose_app l)) in
+ let rargs = getargs rhs
+ and largs = getargs lhs in
+ List.fold_right2
+ (solveArg eqonleft op) largs rargs
+ (Tacticals.New.tclTHEN (choose_eq eqonleft) h_reflexivity)
+ end
end
begin function
| PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!"))
@@ -155,16 +157,18 @@ let hd_app c = match kind_of_term c with
let decideGralEquality =
Proofview.tclORELSE
begin
- Proofview.Goal.concl >>= fun concl ->
- match_eqdec concl >= fun eqonleft,_,c1,c2,typ ->
- Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>= fun headtyp ->
- begin match kind_of_term headtyp with
- | Ind mi -> Proofview.tclUNIT mi
- | _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects."))
- end >= fun rectype ->
- (Tacticals.New.tclTHEN
- (mkBranches c1 c2)
- (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ match_eqdec concl >= fun eqonleft,_,c1,c2,typ ->
+ Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) >>= fun headtyp ->
+ begin match kind_of_term headtyp with
+ | Ind mi -> Proofview.tclUNIT mi
+ | _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects."))
+ end >= fun rectype ->
+ (Tacticals.New.tclTHEN
+ (mkBranches c1 c2)
+ (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
+ end
end
begin function
| PatternMatchingFailure ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ff35b4eeb..782ca67d5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -324,7 +324,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
| _ -> assert false
let type_of_clause = function
- | None -> Proofview.Goal.concl
+ | None -> Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (Proofview.Goal.concl gl))
| Some id -> Tacmach.New.pf_get_hyp_typ id
let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
@@ -359,8 +359,9 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
if occs != AllOccurrences then (
rewrite_side_tac (Hook.get forward_general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
else
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
+ Proofview.Goal.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
let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
match match_with_equality_type t with
@@ -391,6 +392,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
| None -> Proofview.tclZERO e
(* error "The provided term does not end with an equality or a declared rewrite relation." *)
end
+ end
let general_rewrite_ebindings =
general_rewrite_ebindings_clause None
@@ -465,13 +467,16 @@ type delayed_open_constr_with_bindings =
let general_multi_multi_rewrite with_evars l cl tac =
let do1 l2r f =
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- try (* f (an interpretation function) can raise exceptions *)
- let sigma,c = f env sigma in
- Tacticals.New.tclWITHHOLES with_evars
- (general_multi_rewrite l2r with_evars ?tac c) sigma cl
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ try (* f (an interpretation function) can raise exceptions *)
+ let sigma,c = f env sigma in
+ Tacticals.New.tclWITHHOLES with_evars
+ (general_multi_rewrite l2r with_evars ?tac c) sigma cl
+ with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
+ in
let rec doN l2r c = function
| Precisely n when n <= 0 -> Proofview.tclUNIT ()
| Precisely 1 -> do1 l2r c
@@ -848,15 +853,17 @@ 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.env >>= fun env ->
- Proofview.Goal.concl >>= fun concl ->
- match find_positions env sigma t1 t2 with
+ Proofview.Goal.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
| Inr _ ->
Proofview.tclZERO (Errors.UserError ("discr" , str"Not a discriminable equality."))
| Inl (cpath, (_,dirn), _) ->
Tacmach.New.pf_apply get_type_of >>= fun get_type_of ->
let sort = get_type_of concl in
discr_positions env sigma u eq_clause cpath dirn sort
+ end
let onEquality with_evars tac (c,lbindc) =
Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
@@ -877,16 +884,18 @@ let onEquality with_evars tac (c,lbindc) =
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
let onNegatedEquality with_evars tac =
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.concl >>= fun ccl ->
- Proofview.Goal.env >>= fun env ->
- match kind_of_term (hnf_constr env sigma ccl) with
- | Prod (_,t,u) when is_empty_type u ->
- Tacticals.New.tclTHEN introf
- (Tacticals.New.onLastHypId (fun id ->
- onEquality with_evars tac (mkVar id,NoBindings)))
- | _ ->
- Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality."))
+ Proofview.Goal.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
+ match kind_of_term (hnf_constr env sigma ccl) with
+ | Prod (_,t,u) when is_empty_type u ->
+ Tacticals.New.tclTHEN introf
+ (Tacticals.New.onLastHypId (fun id ->
+ onEquality with_evars tac (mkVar id,NoBindings)))
+ | _ ->
+ Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality."))
+ end
let discrSimpleClause with_evars = function
| None -> onNegatedEquality with_evars discrEq
@@ -1268,9 +1277,10 @@ let injConcl = injClause None false None
let injHyp id = injClause None false (Some (ElimOnIdent (Loc.ghost,id)))
let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
- Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>= fun sort ->
+ Proofview.Goal.enter begin fun gl ->
+ Tacmach.New.of_old (fun gls -> pf_apply get_type_of gls (pf_concl gls)) >>= fun sort ->
let sigma = clause.evd in
- Proofview.Goal.env >>= fun env ->
+ let env = Proofview.Goal.env gl in
match find_positions env sigma t1 t2 with
| Inl (cpath, (_,dirn), _) ->
discr_positions env sigma u clause cpath dirn sort
@@ -1279,6 +1289,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
let dEqThen with_evars ntac = function
| None -> onNegatedEquality with_evars (decompEqThen ntac)
@@ -1514,9 +1525,10 @@ 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.env >>= fun env ->
- Proofview.Goal.hyps >>= fun hyps ->
- Proofview.Goal.concl >>= fun concl ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let hyps = Proofview.Goal.hyps gl in
+ let concl = Proofview.Goal.concl gl in
let hyps = Environ.named_context_of_val hyps in
(* The set of hypotheses using x *)
let depdecls =
@@ -1551,29 +1563,32 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
else
[Proofview.tclUNIT ()]) @
[Proofview.V82.tactic (tclTRY (clear [x;hyp]))])
+ 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.hyps >>= fun hyps ->
- let hyps = Environ.named_context_of_val hyps in
- Tacmach.New.pf_get_hyp x >>= fun (_,xval,_) ->
- (* If x has a body, simply replace x with body and clear x *)
- if not (Option.is_empty xval) then Proofview.V82.tactic (tclTHEN (unfold_body x) (clear [x])) else
- (* x is a variable: *)
- let varx = mkVar x in
- (* Find a non-recursive definition for x *)
- let found gl =
- try
- let test hyp _ = is_eq_x gl varx hyp in
- Context.fold_named_context test ~init:() hyps;
- errorlabstrm "Subst"
- (str "Cannot find any non-recursive equality over " ++ pr_id x ++
- str".")
- with FoundHyp res -> res in
- Tacmach.New.of_old found >>= fun (hyp,rhs,dir) ->
- subst_one dep_proof_ok x (hyp,rhs,dir)
+ Proofview.Goal.enter begin fun gl ->
+ let hyps = Proofview.Goal.hyps gl in
+ let hyps = Environ.named_context_of_val hyps in
+ Tacmach.New.pf_get_hyp x >>= fun (_,xval,_) ->
+ (* If x has a body, simply replace x with body and clear x *)
+ if not (Option.is_empty xval) then Proofview.V82.tactic (tclTHEN (unfold_body x) (clear [x])) else
+ (* x is a variable: *)
+ let varx = mkVar x in
+ (* Find a non-recursive definition for x *)
+ let found gl =
+ try
+ let test hyp _ = is_eq_x gl varx hyp in
+ Context.fold_named_context test ~init:() hyps;
+ errorlabstrm "Subst"
+ (str "Cannot find any non-recursive equality over " ++ pr_id x ++
+ str".")
+ with FoundHyp res -> res in
+ Tacmach.New.of_old found >>= fun (hyp,rhs,dir) ->
+ subst_one dep_proof_ok x (hyp,rhs,dir)
+ end
let subst_gen dep_proof_ok ids =
Tacticals.New.tclTHEN (Proofview.V82.tactic tclNORMEVAR) (Tacticals.New.tclMAP (subst_one_var dep_proof_ok) ids)
@@ -1651,9 +1666,11 @@ let rewrite_multi_assumption_cond cond_eq_term cl =
with | Failure _ | UserError _ -> arec rest
end
in
- Proofview.Goal.hyps >>= fun hyps ->
- let hyps = Environ.named_context_of_val hyps in
- arec hyps
+ Proofview.Goal.enter begin fun gl ->
+ let hyps = Proofview.Goal.hyps gl in
+ let hyps = Environ.named_context_of_val hyps in
+ arec hyps
+ end
let replace_multi_term dir_opt c =
let cond_eq_fun =
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 0555564bd..20f72b3d5 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -53,8 +53,10 @@ let instantiate n (ist,rawc) ido gl =
open Proofview.Notations
let let_evar name typ =
let src = (Loc.ghost,Evar_kinds.GoalEvar) in
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- let sigma',evar = Evarutil.new_evar sigma env ~src typ in
- Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
- (Tactics.letin_tac None name evar None Locusops.nowhere)
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let sigma',evar = Evarutil.new_evar sigma env ~src typ in
+ Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
+ (Tactics.letin_tac None name evar None Locusops.nowhere)
+ end
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a4765f22b..fcb131161 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -664,9 +664,9 @@ let mkCaseEq a : unit Proofview.tactic =
Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) >>= fun type_of_a ->
Tacticals.New.tclTHENLIST
[Proofview.V82.tactic (Hiddentac.h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
- begin
- Proofview.Goal.concl >>= fun concl ->
- Proofview.Goal.env >>= fun env ->
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ let env = Proofview.Goal.env gl in
Proofview.V82.tactic begin
change_in_concl None
(Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl)
@@ -683,8 +683,8 @@ let case_eq_intros_rewrite x =
(* Pp.msgnl (Printer.pr_lconstr x); *)
Tacticals.New.tclTHENLIST [
mkCaseEq x;
- begin
- Proofview.Goal.concl >>= fun concl ->
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
Tacmach.New.pf_ids_of_hyps >>= fun hyps ->
let n' = nb_prod concl in
Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) >>= fun h ->
@@ -719,7 +719,7 @@ let destauto_in id =
destauto ctype
TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Proofview.Goal.concl >>= fun concl -> destauto concl ]
+| [ "destauto" ] -> [ Proofview.Goal.enter (fun gl -> destauto (Proofview.Goal.concl gl)) ]
| [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
END
diff --git a/tactics/inv.ml b/tactics/inv.ml
index e4d4fc80e..b3c8b2837 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -443,44 +443,46 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
let raw_inversion inv_kind id status names =
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- Proofview.Goal.concl >>= fun concl ->
- let c = mkVar id in
- Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind >>= fun reduce_to_atomic_ind ->
- Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
- begin
- try
- Proofview.tclUNIT (reduce_to_atomic_ind (type_of c))
- with UserError _ ->
- Proofview.tclZERO (Errors.UserError ("raw_inversion" ,
- str ("The type of "^(Id.to_string id)^" is not inductive.")))
- end >= fun (ind,t) ->
- Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>= fun indclause ->
- let ccl = clenv_type indclause in
- check_no_metas indclause ccl;
- let IndType (indf,realargs) = find_rectype env sigma ccl in
- let (elim_predicate,neqns) =
- make_inv_predicate env sigma indf realargs id status concl in
- let (cut_concl,case_tac) =
- if status != NoDep & (dependent c concl) then
- Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])),
- Tacticals.New.case_then_using
- else
- Reduction.beta_appvect elim_predicate (Array.of_list realargs),
- Tacticals.New.case_nodep_then_using
- in
- (Tacticals.New.tclTHENS
- (assert_tac Anonymous cut_concl)
- [case_tac names
- (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
- (Some elim_predicate) ([],[]) ind indclause;
- Tacticals.New.onLastHypId
- (fun id ->
- (Tacticals.New.tclTHEN
- (Proofview.V82.tactic (apply_term (mkVar id)
- (List.init neqns (fun _ -> Evarutil.mk_new_meta()))))
- reflexivity))])
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let concl = Proofview.Goal.concl gl in
+ let c = mkVar id in
+ Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind >>= fun reduce_to_atomic_ind ->
+ Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+ begin
+ try
+ Proofview.tclUNIT (reduce_to_atomic_ind (type_of c))
+ with UserError _ ->
+ Proofview.tclZERO (Errors.UserError ("raw_inversion" ,
+ str ("The type of "^(Id.to_string id)^" is not inductive.")))
+ end >= fun (ind,t) ->
+ Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c,t)) >>= fun indclause ->
+ let ccl = clenv_type indclause in
+ check_no_metas indclause ccl;
+ let IndType (indf,realargs) = find_rectype env sigma ccl in
+ let (elim_predicate,neqns) =
+ make_inv_predicate env sigma indf realargs id status concl in
+ let (cut_concl,case_tac) =
+ if status != NoDep & (dependent c concl) then
+ Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])),
+ Tacticals.New.case_then_using
+ else
+ Reduction.beta_appvect elim_predicate (Array.of_list realargs),
+ Tacticals.New.case_nodep_then_using
+ in
+ (Tacticals.New.tclTHENS
+ (assert_tac Anonymous cut_concl)
+ [case_tac names
+ (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
+ (Some elim_predicate) ([],[]) ind indclause;
+ Tacticals.New.onLastHypId
+ (fun id ->
+ (Tacticals.New.tclTHEN
+ (Proofview.V82.tactic (apply_term (mkVar id)
+ (List.init neqns (fun _ -> Evarutil.mk_new_meta()))))
+ reflexivity))])
+ end
(* Error messages of the inversion tactics *)
let wrap_inv_error id = function
@@ -523,25 +525,29 @@ 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.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
- Proofview.Goal.concl >>= fun concl ->
- let nb_prod_init = nb_prod concl in
- let intros_replace_ids =
- Proofview.Goal.concl >>= fun concl ->
- let nb_of_new_hyp =
- nb_prod concl - (List.length hyps + nb_prod_init)
+ Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
+ 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 ->
+ let concl = Proofview.Goal.concl gl in
+ let nb_of_new_hyp =
+ nb_prod concl - (List.length hyps + nb_prod_init)
+ in
+ if nb_of_new_hyp < 1 then
+ intros_replacing ids
+ else
+ Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids)
+ end
in
- if nb_of_new_hyp < 1 then
- intros_replacing ids
- else
- Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids)
- in
- Proofview.tclORELSE
- (Tacticals.New.tclTHENLIST
- [Proofview.V82.tactic (bring_hyps hyps);
- inversion (false,k) NoDep names id;
- intros_replace_ids])
- (wrap_inv_error id)
+ Proofview.tclORELSE
+ (Tacticals.New.tclTHENLIST
+ [Proofview.V82.tactic (bring_hyps hyps);
+ inversion (false,k) NoDep names id;
+ intros_replace_ids])
+ (wrap_inv_error id)
+ 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 04819830e..e726e7692 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -284,17 +284,19 @@ 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.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
- let intros_replace_ids =
- Proofview.Goal.concl >>= fun concl ->
- let nb_of_new_hyp = nb_prod concl - List.length ids in
- if nb_of_new_hyp < 1 then
- intros_replacing ids
- else
- (Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids))
- in
- ((Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTHEN (bring_hyps hyps) (lemInv id c)))
- (intros_replace_ids)))
+ Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.lift (Goal.sensitive_list_map Tacmach.New.pf_get_hyp_sensitive ids) >>= fun hyps ->
+ let intros_replace_ids =
+ let concl = Proofview.Goal.concl gl in
+ let nb_of_new_hyp = nb_prod concl - List.length ids in
+ if nb_of_new_hyp < 1 then
+ intros_replacing ids
+ else
+ (Tacticals.New.tclTHEN (Tacticals.New.tclDO nb_of_new_hyp intro) (intros_replacing ids))
+ in
+ ((Tacticals.New.tclTHEN (Proofview.V82.tactic (tclTHEN (bring_hyps hyps) (lemInv id c)))
+ (intros_replace_ids)))
+ 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 66b2c64b0..14a9eb0ed 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1764,37 +1764,39 @@ 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.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
- Proofview.Goal.concl >>= fun concl ->
- Proofview.tclORELSE
- begin
- try
- let rel, args = decompose_app_rel env sigma concl in
- let evm = sigma in
- let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
- fn env evm car rel
- with e -> Proofview.tclZERO e
- end
- begin function
- | e ->
- Proofview.tclORELSE
- fallback
- begin function
- | Hipattern.NoEquationFound ->
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let concl = Proofview.Goal.concl gl in
+ Proofview.tclORELSE
+ begin
+ try
+ let rel, args = decompose_app_rel env sigma concl in
+ let evm = sigma in
+ let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
+ fn env evm car rel
+ with e -> Proofview.tclZERO e
+ end
+ begin function
+ | e ->
+ Proofview.tclORELSE
+ fallback
+ begin function
+ | Hipattern.NoEquationFound ->
(* spiwack: [Errors.push] here is unlikely to do what
it's intended to, or anything meaningful for that
matter. *)
- let e = Errors.push e in
- begin match e with
- | Not_found ->
- let rel, args = decompose_app_rel env sigma concl in
- not_declared env ty rel
- | _ -> Proofview.tclZERO e
- end
- | e' -> Proofview.tclZERO e'
- end
- end
+ let e = Errors.push e in
+ begin match e with
+ | Not_found ->
+ let rel, args = decompose_app_rel env sigma concl in
+ not_declared env ty rel
+ | _ -> Proofview.tclZERO e
+ end
+ | e' -> Proofview.tclZERO e'
+ end
+ end
+ end
let setoid_reflexivity =
setoid_proof "reflexive"
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index abc1daa5b..83958eca2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1265,11 +1265,13 @@ and interp_app loc ist fv largs =
end >>== fun v ->
(* No errors happened, we propagate the trace *)
let v = append_trace trace v in
- Proofview.Goal.env >>== fun env ->
- Proofview.tclLIFT begin
- debugging_step ist
- (fun () ->
- str"evaluation returns"++fnl()++pr_value (Some env) v)
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ Proofview.tclLIFT begin
+ debugging_step ist
+ (fun () ->
+ str"evaluation returns"++fnl()++pr_value (Some env) v)
+ end
end <*>
if List.is_empty lval then (Proofview.Goal.return v) else interp_app loc ist v lval
else
@@ -1343,9 +1345,13 @@ and interp_letin ist llc u =
(* Interprets the Match Context expressions *)
and interp_match_goal ist lz lr lmr =
- Proofview.Goal.enterl begin fun env sigma hyps concl ->
+ Proofview.Goal.enterl begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let hyps = Proofview.Goal.hyps gl in
let hyps = Environ.named_context_of_val hyps in
let hyps = if lr then List.rev hyps else hyps in
+ let concl = Proofview.Goal.concl gl in
let rec apply_goal_sub app ist (id,c) csr mt mhyps hyps =
let rec match_next_pattern next = match IStream.peek next with
| None -> Proofview.tclZERO PatternMatchingFailure
@@ -1428,7 +1434,8 @@ and interp_match_goal ist lz lr lmr =
(* Tries to match the hypotheses in a Match Context *)
and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
- Proofview.Goal.env >>== fun env ->
+ Proofview.Goal.enterl begin fun gl ->
+ let env = Proofview.Goal.env gl in
let rec apply_hyps_context_rec lfun lmatch lhyps_rest = function
| hyp_pat::tl ->
let (hypname, _, pat as hyp_pat) =
@@ -1467,6 +1474,7 @@ and apply_hyps_context ist env lz mt lctxt lgmatch mhyps hyps =
eval_with_fail {ist with lfun=lfun} lz mt
in
apply_hyps_context_rec lctxt lgmatch hyps mhyps
+ end
and interp_external loc ist gl com req la = assert false
(* arnaud: todo
@@ -1582,11 +1590,13 @@ and interp_match ist lz constr lmr =
in
Proofview.tclORELSE begin match matches with
| None -> let e = PatternMatchingFailure in
- (Proofview.Goal.env >>= fun env ->
- Proofview.tclLIFT begin
- debugging_exception_step ist false e (fun () ->
- str "matching with pattern" ++ fnl () ++
- pr_constr_pattern_env env c)
+ (Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ Proofview.tclLIFT begin
+ debugging_exception_step ist false e (fun () ->
+ str "matching with pattern" ++ fnl () ++
+ pr_constr_pattern_env env c)
+ end
end) <*> Proofview.tclZERO e
| Some lmatch ->
Proofview.tclORELSE
@@ -1596,12 +1606,14 @@ and interp_match ist lz constr lmr =
end
begin function
| e ->
- (Proofview.Goal.env >>= fun env ->
- Proofview.tclLIFT begin
- debugging_exception_step ist false e (fun () ->
- str "rule body for pattern" ++
- pr_constr_pattern_env env c)
- end) <*>
+ (Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ Proofview.tclLIFT begin
+ debugging_exception_step ist false e (fun () ->
+ str "rule body for pattern" ++
+ pr_constr_pattern_env env c)
+ end
+ end) <*>
Proofview.tclZERO e
end
end
@@ -1635,7 +1647,9 @@ and interp_match ist lz constr lmr =
Proofview.tclZERO e
end
end >>== fun csr ->
- Proofview.Goal.enterl begin fun env sigma _ _ ->
+ Proofview.Goal.enterl begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
Proofview.tclORELSE
(apply_match ist csr ilr)
@@ -1655,17 +1669,20 @@ and interp_ltac_constr ist e =
(val_interp ist e)
begin function
| Not_found ->
- (Proofview.Goal.env >>= fun env ->
- Proofview.tclLIFT begin
- debugging_step ist (fun () ->
- str "evaluation failed for" ++ fnl() ++
- Pptactic.pr_glob_tactic env e)
+ (Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ Proofview.tclLIFT begin
+ debugging_step ist (fun () ->
+ str "evaluation failed for" ++ fnl() ++
+ Pptactic.pr_glob_tactic env e)
+ end
end) <*>
Proofview.tclZERO Not_found
| e -> Proofview.tclZERO e
end
end >>== fun result ->
- Proofview.Goal.env >>== fun env ->
+ Proofview.Goal.enterl begin fun gl ->
+ let env = Proofview.Goal.env gl in
let result = Value.normalize result in
try
let cresult = coerce_to_closed_constr env result in
@@ -1677,11 +1694,13 @@ and interp_ltac_constr ist e =
end <*>
(Proofview.Goal.return cresult)
with CannotCoerceTo _ ->
- Proofview.Goal.env >>== fun env ->
+ let env = Proofview.Goal.env gl in
Proofview.tclZERO (UserError ( "",
errorlabstrm ""
(str "Must evaluate to a closed term" ++ fnl() ++
str "offending expression: " ++ fnl() ++ pr_inspect env e result)))
+ end
+
(* Interprets tactic expressions : returns a "tactic" *)
and interp_tactic ist tac =
@@ -1701,9 +1720,11 @@ and interp_atomic ist tac =
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
| TacIntroMove (ido,hto) ->
- Proofview.Goal.env >>= fun env ->
- Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>= fun mloc ->
- h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) >>= fun mloc ->
+ h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
+ end
| TacAssumption -> Proofview.V82.tactic h_assumption
| TacExact c ->
Proofview.V82.tactic begin fun gl ->
@@ -1730,7 +1751,9 @@ and interp_atomic ist tac =
gl
end
| TacApply (a,ev,cb,cl) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
try (* interp_open_constr_with_bindings_loc can raise exceptions *)
let sigma, l =
List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
@@ -1745,7 +1768,9 @@ and interp_atomic ist tac =
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
| TacElim (ev,cb,cbo) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
try (* interpretation functions may raise exceptions *)
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
@@ -1761,7 +1786,9 @@ and interp_atomic ist tac =
gl
end
| TacCase (ev,cb) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.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
Tacticals.New.tclWITHHOLES ev (h_case ev) sigma cb
end
@@ -1774,11 +1801,13 @@ and interp_atomic ist tac =
gl
end
| TacFix (idopt,n) ->
- Proofview.Goal.env >>= fun env ->
- Proofview.V82.tactic (h_fix (Option.map (interp_fresh_ident ist env) idopt) n)
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ Proofview.V82.tactic (h_fix (Option.map (interp_fresh_ident ist env) idopt) n)
+ end
| TacMutualFix (id,n,l) ->
- Proofview.Goal.env >>= fun env ->
- Proofview.V82.tactic begin fun gl ->
+ Proofview.V82.tactic begin fun gl ->
+ let env = pf_env gl in
let f sigma (id,n,c) =
let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
sigma , (interp_fresh_ident ist env id,n,c_interp) in
@@ -1794,11 +1823,13 @@ and interp_atomic ist tac =
gl
end
| TacCofix idopt ->
- Proofview.Goal.env >>= fun env ->
- Proofview.V82.tactic (h_cofix (Option.map (interp_fresh_ident ist env) idopt))
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ Proofview.V82.tactic (h_cofix (Option.map (interp_fresh_ident ist env) idopt))
+ end
| TacMutualCofix (id,l) ->
- Proofview.Goal.env >>= fun env ->
- Proofview.V82.tactic begin fun gl ->
+ Proofview.V82.tactic begin fun gl ->
+ let env = pf_env gl in
let f sigma (id,c) =
let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
sigma , (interp_fresh_ident ist env id,c_interp) in
@@ -1822,7 +1853,9 @@ and interp_atomic ist tac =
gl
end
| TacAssert (t,ipat,c) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
try (* intrerpreation function may raise exceptions *)
let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in
Tacmach.New.of_old (fun gl -> interp_intro_pattern ist gl) >>= fun patt ->
@@ -1833,11 +1866,11 @@ and interp_atomic ist tac =
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
| TacGeneralize cl ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
- Proofview.V82.tactic begin fun gl ->
- let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
- tclWITHHOLES false (h_generalize_gen) sigma cl gl
- end
+ Proofview.V82.tactic begin fun gl ->
+ let sigma = project gl in
+ let env = pf_env gl in
+ let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
+ tclWITHHOLES false (h_generalize_gen) sigma cl gl
end
| TacGeneralizeDep c ->
Proofview.V82.tactic begin fun gl ->
@@ -1848,7 +1881,9 @@ and interp_atomic ist tac =
gl
end
| TacLetTac (na,c,clp,b,eqpat) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
Tacmach.New.of_old (fun gl -> interp_clause ist gl clp) >>= fun clp ->
Tacmach.New.of_old (fun gl -> Option.map (interp_intro_pattern ist gl) eqpat) >>= fun eqpat ->
if Locusops.is_nowhere clp then
@@ -1868,13 +1903,17 @@ and interp_atomic ist tac =
(* Automation tactics *)
| TacTrivial (debug,lems,l) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
Auto.h_trivial ~debug
(interp_auto_lemmas ist env sigma lems)
(Option.map (List.map (interp_hint_base ist)) l)
end
| TacAuto (debug,n,lems,l) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
(interp_auto_lemmas ist env sigma lems)
(Option.map (List.map (interp_hint_base ist)) l)
@@ -1884,25 +1923,27 @@ and interp_atomic ist tac =
| TacSimpleInductionDestruct (isrec,h) ->
h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
| TacInductionDestruct (isrec,ev,(l,el,cls)) ->
- Proofview.Goal.env >>= fun env ->
- let l =
- Goal.sensitive_list_map begin fun (c,(ipato,ipats)) ->
- Goal.V82.to_sensitive (fun gl -> interp_induction_arg ist gl c) >- fun c ->
- Goal.V82.to_sensitive (fun gl -> interp_intro_pattern ist gl) >- fun interp_intro_pattern ->
- Goal.return begin
- c,
- (Option.map interp_intro_pattern ipato,
- Option.map interp_intro_pattern ipats)
- end
- end l
- in
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.lift l >>= fun l ->
- let sigma,el =
- Option.fold_map (interp_constr_with_bindings ist env) sigma el in
- Tacmach.New.of_old (fun gl -> interp_clause ist gl) >>= fun interp_clause ->
- let cls = Option.map interp_clause cls in
- Tacticals.New.tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls)
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let l =
+ Goal.sensitive_list_map begin fun (c,(ipato,ipats)) ->
+ Goal.V82.to_sensitive (fun gl -> interp_induction_arg ist gl c) >- fun c ->
+ Goal.V82.to_sensitive (fun gl -> interp_intro_pattern ist gl) >- fun interp_intro_pattern ->
+ Goal.return begin
+ c,
+ (Option.map interp_intro_pattern ipato,
+ Option.map interp_intro_pattern ipats)
+ end
+ end l
+ in
+ let sigma = Proofview.Goal.sigma gl in
+ Proofview.Goal.lift l >>= fun l ->
+ let sigma,el =
+ Option.fold_map (interp_constr_with_bindings ist env) sigma el in
+ Tacmach.New.of_old (fun gl -> interp_clause ist gl) >>= fun interp_clause ->
+ let cls = Option.map interp_clause cls in
+ Tacticals.New.tclWITHHOLES ev (h_induction_destruct isrec ev) sigma (l,el,cls)
+ end
| TacDoubleInduction (h1,h2) ->
let h1 = interp_quantified_hypothesis ist h1 in
let h2 = interp_quantified_hypothesis ist h2 in
@@ -1924,7 +1965,9 @@ and interp_atomic ist tac =
(Proofview.V82.tclEVARS sigma)
(Elim.h_decompose l c_interp)
| TacSpecialize (n,cb) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
Proofview.V82.tactic begin fun gl ->
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
tclWITHHOLES false (h_specialize n) sigma cb gl
@@ -1953,8 +1996,8 @@ and interp_atomic ist tac =
h_move dep (interp_hyp ist gl id1) (interp_move_location ist gl id2) gl
end
| TacRename l ->
- Proofview.Goal.env >>= fun env ->
- Proofview.V82.tactic begin fun gl ->
+ Proofview.V82.tactic begin fun gl ->
+ let env = pf_env gl in
h_rename (List.map (fun (id1,id2) ->
interp_hyp ist gl id1,
interp_fresh_ident ist env (snd id2)) l)
@@ -1967,24 +2010,32 @@ and interp_atomic ist tac =
(* Constructors *)
| TacLeft (ev,bl) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let sigma, bl = interp_bindings ist env sigma bl in
Tacticals.New.tclWITHHOLES ev (h_left ev) sigma bl
end
| TacRight (ev,bl) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let sigma, bl = interp_bindings ist env sigma bl in
Tacticals.New.tclWITHHOLES ev (h_right ev) sigma bl
end
| TacSplit (ev,_,bll) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.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
Tacticals.New.tclWITHHOLES ev (h_split ev) sigma bll
end
| TacAnyConstructor (ev,t) ->
Tactics.any_constructor ev (Option.map (interp_tactic ist) t)
| TacConstructor (ev,n,bl) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let sigma, bl = interp_bindings ist env sigma bl in
Tacticals.New.tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl
end
@@ -2019,7 +2070,9 @@ and interp_atomic ist tac =
gl
end
| TacChange (Some op,c,cl) ->
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
Proofview.V82.tactic begin fun gl ->
let sign,op = interp_typed_pattern ist env sigma op in
(* spiwack: (2012/04/18) the evar_map output by pf_interp_constr
@@ -2104,7 +2157,8 @@ and interp_atomic ist tac =
Proofview.V82.tclEVARS sigma <*>
tac args ist
| TacAlias (loc,s,l,(_,body)) ->
- Proofview.Goal.env >>= fun env ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
let rec f x = match genarg_tag x with
| IntOrVarArgType ->
(Proofview.Goal.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)))
@@ -2195,6 +2249,7 @@ and interp_atomic ist tac =
lfun = lfun;
extra = TacStore.set ist.extra f_trace trace; } in
interp_tactic ist body
+ end
(* Initial call for interpretation *)
@@ -2211,7 +2266,9 @@ let eval_tactic t =
let interp_tac_gen lfun avoid_ids debug t =
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let extra = TacStore.set TacStore.empty f_debug debug in
let extra = TacStore.set extra f_avoid_ids avoid_ids in
let ist = { lfun = lfun; extra = extra } in
@@ -2232,7 +2289,9 @@ let eval_ltac_constr t =
(* Used to hide interpretation for pretty-print, now just launch tactics *)
let hide_interp t ot =
- Proofview.Goal.enter begin fun env sigma _ _ ->
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
gsigma = sigma; genv = env } in
let te = intern_pure_tactic ist t in
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 74c31fa38..5d3c8b97a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -522,27 +522,35 @@ module New = struct
| e -> Proofview.tclZERO e
end
- let nthDecl m =
- Proofview.Goal.hyps >>== fun hyps ->
+ let nthDecl m gl =
+ let hyps = Proofview.Goal.hyps gl in
try
let hyps = Environ.named_context_of_val hyps in
- (Proofview.Goal.return (List.nth hyps (m-1)))
- with Failure _ -> tclZERO (UserError ("" , Pp.str"No such assumption."))
+ List.nth hyps (m-1)
+ with Failure _ -> Errors.error "No such assumption."
- let nthHypId m = nthDecl m >>== fun (id,_,_) ->
- Proofview.Goal.return id
- let nthHyp m = nthHypId m >>== fun id ->
- Proofview.Goal.return (mkVar id)
+ let nthHypId m gl =
+ let (id,_,_) = nthDecl m gl in
+ id
+ let nthHyp m gl =
+ mkVar (nthHypId m gl)
let onNthHypId m tac =
- nthHypId m >>= tac
+ Goal.enter begin fun gl ->
+ Proofview.tclUNIT (nthHypId m gl) >= tac
+ end
let onNthHyp m tac =
- nthHyp m >>= tac
+ Goal.enter begin fun gl ->
+ Proofview.tclUNIT (nthHyp m gl) >= tac
+ end
let onLastHypId = onNthHypId 1
let onLastHyp = onNthHyp 1
- let onNthDecl m tac = nthDecl m >>= tac
+ let onNthDecl m tac =
+ Proofview.Goal.enter begin fun gl ->
+ Proofview.tclUNIT (nthDecl m gl) >= tac
+ end
let onLastDecl = onNthDecl 1
let ifOnHyp pred tac1 tac2 id =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fe605da8e..5e62451f9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -460,8 +460,9 @@ let build_intro_tac id dest tac = match dest with
| dest -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (introduction id); Proofview.V82.tactic (move_hyp true id dest); tac id]
let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
- Proofview.Goal.concl >>= fun concl ->
- match kind_of_term concl with
+ Proofview.Goal.enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
+ match kind_of_term concl with
| Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
find_name loc (name,None,t) name_flag >>= fun name ->
build_intro_tac name move_flag tac
@@ -476,14 +477,15 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac =
(* probably also a pity that intro does zeta *)
else Proofview.tclUNIT ()
end <*>
- Proofview.tclORELSE
+ Proofview.tclORELSE
(Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl)
- (intro_then_gen loc name_flag move_flag false dep_flag tac))
+ (intro_then_gen loc name_flag move_flag false dep_flag tac))
begin function
| RefinerError IntroNeedsProduct ->
Proofview.tclZERO (Loc.add_loc (Errors.UserError("Intro",str "No product even after head-reduction.")) loc)
| e -> Proofview.tclZERO e
end
+ end
let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> Proofview.tclUNIT ())
let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) MoveLast true false
@@ -1281,18 +1283,20 @@ let check_number_of_constructors expctdnumopt i nconstr =
if i > nconstr then error "Not enough constructors."
let constructor_tac with_evars expctdnumopt i lbind =
- Proofview.Goal.concl >>= fun cl ->
- Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
- try (* reduce_to_quantified_ind can raise an exception *)
- let (mind,redcl) = reduce_to_quantified_ind cl in
- let nconstr =
- Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
- check_number_of_constructors expctdnumopt i nconstr;
- let cons = mkConstruct (ith_constructor_of_inductive mind i) in
- let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in
- (Tacticals.New.tclTHENLIST
- [Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ Proofview.Goal.enter begin fun gl ->
+ let cl = Proofview.Goal.concl gl in
+ Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
+ try (* reduce_to_quantified_ind can raise an exception *)
+ let (mind,redcl) = reduce_to_quantified_ind cl in
+ let nconstr =
+ Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
+ check_number_of_constructors expctdnumopt i nconstr;
+ let cons = mkConstruct (ith_constructor_of_inductive mind i) in
+ let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in
+ (Tacticals.New.tclTHENLIST
+ [Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
+ with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
let one_constructor i lbind = constructor_tac false None i lbind
@@ -1303,18 +1307,20 @@ let one_constructor i lbind = constructor_tac false None i lbind
let any_constructor with_evars tacopt =
let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
- Proofview.Goal.concl >>= fun cl ->
- Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
+ Proofview.Goal.enter begin fun gl ->
+ let cl = Proofview.Goal.concl gl in
+ Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind >>= fun reduce_to_quantified_ind ->
try (* reduce_to_quantified_ind can raise an exception *)
- let mind = fst (reduce_to_quantified_ind cl) in
- let nconstr =
- Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
- if Int.equal nconstr 0 then error "The type has no constructors.";
- Tacticals.New.tclFIRST
- (List.map
- (fun i -> Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t)
- (List.interval 1 nconstr))
+ let mind = fst (reduce_to_quantified_ind cl) in
+ let nconstr =
+ Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
+ if Int.equal nconstr 0 then error "The type has no constructors.";
+ Tacticals.New.tclFIRST
+ (List.map
+ (fun i -> Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t)
+ (List.interval 1 nconstr))
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ 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
@@ -1400,29 +1406,31 @@ let rewrite_hyp l2r id =
Hook.get forward_subst_one true x (id,rhs,l2r) in
let clear_var_and_eq c =
tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
- Proofview.Goal.env >>= fun env ->
- Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
- Tacmach.New.pf_apply whd_betadeltaiota >>= fun whd_betadeltaiota ->
- try (* type_of can raise an exception *)
- let t = whd_betadeltaiota (type_of (mkVar id)) in
- (* TODO: detect setoid equality? better detect the different equalities *)
- match match_with_equality_type t with
- | Some (hdcncl,[_;lhs;rhs]) ->
- if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then
- subst_on l2r (destVar lhs) rhs
- else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then
- subst_on l2r (destVar rhs) lhs
- else
- Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
- | Some (hdcncl,[c]) ->
- let l2r = not l2r in (* equality of the form eq_true *)
- if isVar c then
- Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (Proofview.V82.tactic (clear_var_and_eq c))
- else
- Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
- | _ ->
- Proofview.tclZERO (Errors.UserError ("",Pp.str"Cannot find a known equation."))
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
+ Tacmach.New.pf_apply whd_betadeltaiota >>= fun whd_betadeltaiota ->
+ try (* type_of can raise an exception *)
+ let t = whd_betadeltaiota (type_of (mkVar id)) in
+ (* TODO: detect setoid equality? better detect the different equalities *)
+ match match_with_equality_type t with
+ | Some (hdcncl,[_;lhs;rhs]) ->
+ if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then
+ subst_on l2r (destVar lhs) rhs
+ else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then
+ subst_on l2r (destVar rhs) lhs
+ else
+ Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
+ | Some (hdcncl,[c]) ->
+ let l2r = not l2r in (* equality of the form eq_true *)
+ if isVar c then
+ Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (Proofview.V82.tactic (clear_var_and_eq c))
+ else
+ Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
+ | _ ->
+ Proofview.tclZERO (Errors.UserError ("",Pp.str"Cannot find a known equation."))
+ with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ end
let rec explicit_intro_names = function
| (_, IntroIdentifier id) :: l ->
@@ -1893,47 +1901,49 @@ let letin_abstract id c (test,out) (occs,check_occs) gl =
(depdecls,lastlhyp,ccl,out test)
let letin_tac_gen with_eq name (sigmac,c) test ty occs =
- Proofview.Goal.env >>= fun env ->
- Proofview.Goal.hyps >>= fun hyps ->
- let hyps = Environ.named_context_of_val hyps in
- let id =
- let t = match ty with Some t -> t | None -> typ_of env sigmac c in
- let x = id_of_name_using_hdchar (Global.env()) t name in
- if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) else
- Proofview.Goal.lift begin
- if not (mem_named_context x hyps) then Goal.return x else
- error ("The variable "^(Id.to_string x)^" is already declared.")
- end in
- id >>= fun id ->
- Tacmach.New.of_old (letin_abstract id c test occs) >>= fun (depdecls,lastlhyp,ccl,c) ->
- let t = match ty with Some t -> (Proofview.Goal.return t) | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) in
- t >>= fun t ->
- let newcl = match with_eq with
- | Some (lr,(loc,ido)) ->
- let heq = match ido with
- | IntroAnonymous -> Tacmach.New.of_old (fresh_id [id] (add_prefix "Heq" id))
- | IntroFresh heq_base -> Tacmach.New.of_old (fresh_id [id] heq_base)
- | IntroIdentifier id -> (Proofview.Goal.return id)
- | _ -> Proofview.tclZERO (UserError ("" , Pp.str"Expect an introduction pattern naming one hypothesis.")) in
- heq >>== fun heq ->
- let eqdata = build_coq_eq_data () in
- let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
- let eq = applist (eqdata.eq,args) in
- let refl = applist (eqdata.refl, [t;mkVar id]) in
- Proofview.Goal.return begin
- mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)),
- Tacticals.New.tclTHEN
- (intro_gen loc (IntroMustBe heq) lastlhyp true false)
- (Proofview.V82.tactic (thin_body [heq;id]))
- end
- | None ->
- (Proofview.Goal.return (mkNamedLetIn id c t ccl, Proofview.tclUNIT ())) in
- newcl >>= fun (newcl,eq_tac) ->
- Tacticals.New.tclTHENLIST
- [ Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
- intro_gen dloc (IntroMustBe id) lastlhyp true false;
- Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
- eq_tac ]
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let hyps = Proofview.Goal.hyps gl in
+ let hyps = Environ.named_context_of_val hyps in
+ let id =
+ let t = match ty with Some t -> t | None -> typ_of env sigmac c in
+ let x = id_of_name_using_hdchar (Global.env()) t name in
+ if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) else
+ Proofview.Goal.lift begin
+ if not (mem_named_context x hyps) then Goal.return x else
+ error ("The variable "^(Id.to_string x)^" is already declared.")
+ end in
+ id >>= fun id ->
+ Tacmach.New.of_old (letin_abstract id c test occs) >>= fun (depdecls,lastlhyp,ccl,c) ->
+ let t = match ty with Some t -> (Proofview.Goal.return t) | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) in
+ t >>= fun t ->
+ let newcl = match with_eq with
+ | Some (lr,(loc,ido)) ->
+ let heq = match ido with
+ | IntroAnonymous -> Tacmach.New.of_old (fresh_id [id] (add_prefix "Heq" id))
+ | IntroFresh heq_base -> Tacmach.New.of_old (fresh_id [id] heq_base)
+ | IntroIdentifier id -> (Proofview.Goal.return id)
+ | _ -> Proofview.tclZERO (UserError ("" , Pp.str"Expect an introduction pattern naming one hypothesis.")) in
+ heq >>== fun heq ->
+ let eqdata = build_coq_eq_data () in
+ let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
+ let eq = applist (eqdata.eq,args) in
+ let refl = applist (eqdata.refl, [t;mkVar id]) in
+ Proofview.Goal.return begin
+ mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)),
+ Tacticals.New.tclTHEN
+ (intro_gen loc (IntroMustBe heq) lastlhyp true false)
+ (Proofview.V82.tactic (thin_body [heq;id]))
+ end
+ | None ->
+ (Proofview.Goal.return (mkNamedLetIn id c t ccl, Proofview.tclUNIT ())) in
+ newcl >>= fun (newcl,eq_tac) ->
+ Tacticals.New.tclTHENLIST
+ [ Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
+ intro_gen dloc (IntroMustBe id) lastlhyp true false;
+ Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
+ eq_tac ]
+ end
let make_eq_test c = (make_eq_test c,fun _ -> c)
@@ -1942,11 +1952,13 @@ let letin_tac with_eq name c ty occs =
letin_tac_gen with_eq name (sigma,c) (make_eq_test c) ty (occs,true)
let letin_pat_tac with_eq name c ty occs =
- Proofview.tclEVARMAP >= fun sigma ->
- Proofview.Goal.env >>= fun env ->
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
letin_tac_gen with_eq name c
(make_pattern_test env sigma c)
ty (occs,true)
+ end
(* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
let forward usetac ipat c =
@@ -2162,6 +2174,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
let params = List.firstn nparams argl in
(* le gl est important pour ne pas préévaluer *)
let rec atomize_one i avoid =
+ Proofview.Goal.enter begin fun gl ->
if not (Int.equal i nparams) then
Tacmach.New.pf_get_hyp_typ hyp0 >>= fun tmptyp0 ->
(* If argl <> [], we expect typ0 not to be quantified, in order to
@@ -2170,7 +2183,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
let indtyp = reduce_to_atomic_ref indref tmptyp0 in
let argl = snd (decompose_app indtyp) in
let c = List.nth argl (i-1) in
- Proofview.Goal.env >>= fun env ->
+ let env = Proofview.Goal.env gl in
match kind_of_term c with
| Var id when not (List.exists (occur_var env id) avoid) ->
atomize_one (i-1) ((mkVar id)::avoid)
@@ -2189,6 +2202,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
(atomize_one (i-1) ((mkVar x)::avoid))
else
Proofview.tclUNIT ()
+ end
in
atomize_one (List.length argl) params
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
@@ -3121,26 +3135,28 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t
hypotheses from the context *)
let apply_induction_in_context hyp0 elim indvars names induct_tac =
- Proofview.Goal.env >>= fun env ->
- Proofview.Goal.concl >>= fun concl ->
- let statuslists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
- let deps = List.map (on_pi3 refresh_universes_strict) deps in
- let tmpcl = it_mkNamedProd_or_LetIn concl deps in
- let dephyps = List.map (fun (id,_,_) -> id) deps in
- let deps_cstr =
- List.fold_left
- (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in
- Tacticals.New.tclTHENLIST
- [
- (* Generalize dependent hyps (but not args) *)
- if deps = [] then Proofview.tclUNIT () else Proofview.V82.tactic (apply_type tmpcl deps_cstr);
- (* clear dependent hyps *)
- Proofview.V82.tactic (thin dephyps);
- (* side-conditions in elim (resp case) schemes come last (resp first) *)
- apply_induction_with_discharge
- induct_tac elim (List.rev indhyps) lhyp0 (List.rev dephyps) names
- (re_intro_dependent_hypotheses statuslists)
- ]
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let concl = Proofview.Goal.concl gl in
+ let statuslists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
+ let deps = List.map (on_pi3 refresh_universes_strict) deps in
+ let tmpcl = it_mkNamedProd_or_LetIn concl deps in
+ let dephyps = List.map (fun (id,_,_) -> id) deps in
+ let deps_cstr =
+ List.fold_left
+ (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in
+ Tacticals.New.tclTHENLIST
+ [
+ (* Generalize dependent hyps (but not args) *)
+ if deps = [] then Proofview.tclUNIT () else Proofview.V82.tactic (apply_type tmpcl deps_cstr);
+ (* clear dependent hyps *)
+ Proofview.V82.tactic (thin dephyps);
+ (* side-conditions in elim (resp case) schemes come last (resp first) *)
+ apply_induction_with_discharge
+ induct_tac elim (List.rev indhyps) lhyp0 (List.rev dephyps) names
+ (re_intro_dependent_hypotheses statuslists)
+ ]
+ end
(* Induction with several induction arguments, main differences with
induction_from_context is that there is no main induction argument,
@@ -3280,22 +3296,26 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
(induction_with_atomization_of_ind_arg
isrec with_evars elim names (id,lbind) inhyps)
| _ ->
- Proofview.tclEVARMAP >= fun defs ->
- Proofview.Goal.env >>= fun env ->
- let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c)
- Anonymous in
- Tacmach.New.of_old (fresh_id [] x) >>= fun id ->
+ Proofview.Goal.enter begin fun gl ->
+ let defs = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c)
+ Anonymous in
+ Tacmach.New.of_old (fresh_id [] x) >>= fun id ->
(* We need the equality name now *)
- let with_eq = Option.map (fun eq -> (false,eq)) eqname in
+ let with_eq = Option.map (fun eq -> (false,eq)) eqname in
(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
- Proofview.Goal.env >>= fun env ->
- Tacticals.New.tclTHEN
- (* Warning: letin is buggy when c is not of inductive type *)
- (letin_tac_gen with_eq (Name id) (sigma,c)
- (make_pattern_test env defs (sigma,c))
- None (Option.default allHypsAndConcl cls,false))
- (induction_with_atomization_of_ind_arg
- isrec with_evars elim names (id,lbind) inhyps)
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ Tacticals.New.tclTHEN
+ (* Warning: letin is buggy when c is not of inductive type *)
+ (letin_tac_gen with_eq (Name id) (sigma,c)
+ (make_pattern_test env defs (sigma,c))
+ None (Option.default allHypsAndConcl cls,false))
+ (induction_with_atomization_of_ind_arg
+ isrec with_evars elim names (id,lbind) inhyps)
+ end
+ end
(* Induction on a list of arguments. First make induction arguments
atomic (using letins), then do induction. The specificity here is
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 3976fcf14..bc756eb82 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -594,24 +594,26 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Ci a1 ... an = Ci b1 ... bn
replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto
*)
- Proofview.Goal.concl >>= fun gl ->
- match (kind_of_term gl) with
- | App (c,ca) -> (
- match (kind_of_term c) with
- | Ind indeq ->
- if eq_gr (IndRef indeq) Coqlib.glob_eq
- then
- Tacticals.New.tclTHEN
- (do_replace_bl bl_scheme_key ind
- (!avoid)
- nparrec (ca.(2))
- (ca.(1)))
- Auto.default_auto
- else
- Proofview.tclZERO (UserError ("",str"Failure while solving Boolean->Leibniz."))
+ Proofview.Goal.enter begin fun gls ->
+ let gl = Proofview.Goal.concl gls in
+ match (kind_of_term gl) with
+ | App (c,ca) -> (
+ match (kind_of_term c) with
+ | Ind indeq ->
+ if eq_gr (IndRef indeq) Coqlib.glob_eq
+ then
+ Tacticals.New.tclTHEN
+ (do_replace_bl bl_scheme_key ind
+ (!avoid)
+ nparrec (ca.(2))
+ (ca.(1)))
+ Auto.default_auto
+ else
+ Proofview.tclZERO (UserError ("",str"Failure while solving Boolean->Leibniz."))
+ | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz."))
+ )
| _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz."))
- )
- | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz."))
+ end
]
@@ -713,21 +715,23 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
Tacticals.New.tclTHENLIST [Proofview.V82.tactic (apply (andb_true_intro()));
simplest_split ;Auto.default_auto ]
);
- Proofview.Goal.concl >>= fun gl ->
- (* assume the goal to be eq (eq_type ...) = true *)
+ Proofview.Goal.enter begin fun gls ->
+ let gl = Proofview.Goal.concl gls in
+ (* assume the goal to be eq (eq_type ...) = true *)
match (kind_of_term gl) with
- | App(c,ca) -> (match (kind_of_term ca.(1)) with
- | App(c',ca') ->
- let n = Array.length ca' in
- do_replace_lb lb_scheme_key
- (!avoid)
- nparrec
- ca'.(n-2) ca'.(n-1)
- | _ ->
- Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean."))
- )
+ | App(c,ca) -> (match (kind_of_term ca.(1)) with
+ | App(c',ca') ->
+ let n = Array.length ca' in
+ do_replace_lb lb_scheme_key
+ (!avoid)
+ nparrec
+ ca'.(n-2) ca'.(n-1)
| _ ->
Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean."))
+ )
+ | _ ->
+ Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean."))
+ end
]
let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 15:41:53 +0000