aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-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
5 files changed, 292 insertions, 274 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 20:03:30 +0000