aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml6
-rw-r--r--plugins/firstorder/instances.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/recdef.ml6
-rw-r--r--plugins/omega/coq_omega.ml4
-rw-r--r--tactics/auto.ml6
-rw-r--r--tactics/contradiction.ml2
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/hiddentac.mli2
-rw-r--r--tactics/rewrite.ml2
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--tactics/tactics.ml45
-rw-r--r--tactics/tactics.mli2
13 files changed, 52 insertions, 35 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 6b5cb7492..db53dc932 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -243,7 +243,7 @@ let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_aut
let justification tac gls=
tclORELSE
- (tclSOLVE [tclTHEN tac assumption])
+ (tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)])
(fun gls ->
if get_strictness () then
error "Insufficient justification."
@@ -1326,7 +1326,7 @@ let end_tac et2 gls =
(fun c -> tclTHENLIST
[my_refine c;
clear clauses;
- justification assumption])
+ justification (Proofview.V82.of_tactic assumption)])
(initial_instance_stack clauses) [pi.per_casee] 0 tree
| ET_Induction,EK_dep tree ->
let nargs = (List.length pi.per_args) in
@@ -1347,7 +1347,7 @@ let end_tac et2 gls =
[clear [fix_id];
my_refine c;
clear clauses;
- justification assumption])
+ justification (Proofview.V82.of_tactic assumption)])
(initial_instance_stack clauses)
[mkVar c_id] 0 tree] gls0
end
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 0acdc4c80..d34edb863 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -150,7 +150,7 @@ let left_instance_tac (inst,id) continue seq=
Proofview.V82.of_tactic introf;
tclSOLVE [wrap 1 false continue
(deepen (record (id,None) seq))]];
- tclTRY assumption]
+ tclTRY (Proofview.V82.of_tactic assumption)]
| Real((m,t) as c,_)->
if lookup (id,Some c) seq then
tclFAIL 0 (Pp.str "already done")
@@ -182,7 +182,7 @@ let right_instance_tac inst continue seq=
Proofview.V82.of_tactic (split (ImplicitBindings
[mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
tclSOLVE [wrap 0 true continue (deepen seq)]];
- tclTRY assumption]
+ tclTRY (Proofview.V82.of_tactic assumption)]
| Real ((0,t),_) ->
(tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [t])))
(tclSOLVE [wrap 0 true continue (deepen seq)]))
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8c2fdb7eb..3d74c5bc9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -120,7 +120,7 @@ type body_info = constr dynamic_info
let finish_proof dynamic_infos g =
observe_tac "finish"
- ( h_assumption)
+ (Proofview.V82.of_tactic h_assumption)
g
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 881d930fc..64bf71ec6 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -517,7 +517,7 @@ let rec prove_lt hyple g =
(
tclTHENLIST[
apply (delayed_force lt_S_n);
- (observe_tac (str "assumption: " ++ Printer.pr_goal g) (h_assumption))
+ (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic h_assumption))
])
)
end
@@ -757,7 +757,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
tclTHENS (* proof of args < formal args *)
(apply (Lazy.force expr_info.acc_inv))
[
- observe_tac (str "h_assumption") h_assumption;
+ observe_tac (str "h_assumption") (Proofview.V82.of_tactic h_assumption);
tclTHENLIST
[
tclTRY(list_rewrite true
@@ -802,7 +802,7 @@ let rec prove_le g =
(List.hd args,List.hd (List.tl args))
in
tclFIRST[
- h_assumption;
+ Proofview.V82.of_tactic h_assumption;
apply (delayed_force le_n);
begin
try
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 26d252726..98baf7b2a 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1058,7 +1058,7 @@ let replay_history tactic_normalisation =
Proofview.V82.tactic (simpl_in_concl);
intro;
(absurd not_sup_sup) ])
- [ Proofview.V82.tactic assumption ; reflexivity ]
+ [ assumption ; reflexivity ]
in
let theorem =
mkApp (Lazy.force coq_OMEGA2, [|
@@ -1127,7 +1127,7 @@ let replay_history tactic_normalisation =
(intros_using [aux]);
Proofview.V82.tactic (resolve_id aux);
Proofview.V82.tactic (mk_then tac);
- Proofview.V82.tactic assumption ] ;
+ assumption ] ;
Tacticals.New.tclTHENLIST [
Proofview.V82.tactic (unfold sp_Zgt);
Proofview.V82.tactic simpl_in_concl;
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1205d9700..e87158bdd 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1270,7 +1270,7 @@ let exists_evaluable_reference env = function
| EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
let dbg_intro dbg = new_tclLOG dbg (fun () -> str "intro") intro
-let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
+let dbg_assumption dbg = new_tclLOG dbg (fun () -> str "assumption") assumption
let rec trivial_fail_db dbg mod_delta db_list local_db =
let intro_tac =
@@ -1286,7 +1286,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
Tacticals.New.tclFIRST
- ((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac::
+ ((dbg_assumption dbg)::intro_tac::
(List.map Tacticals.New.tclCOMPLETE
(trivial_resolve dbg mod_delta db_list local_db concl)))
end
@@ -1441,7 +1441,7 @@ let search d n mod_delta db_list local_db =
each goal. Hence the [tclEXTEND] *)
Proofview.tclEXTEND [] begin
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 (dbg_assumption d)
(Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
( Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 19e5906f8..0198fc3fd 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -91,7 +91,7 @@ let contradiction_term (c,lbind as cl) =
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))
+ Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption)
else
Proofview.tclORELSE
begin
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 36cb55e5b..7c72d8ad5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -531,8 +531,8 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
(Tacticals.New.tclTRY (general_multi_rewrite false false (mkVar id,NoBindings) clause))
(Proofview.V82.tactic (clear [id])));
Tacticals.New.tclFIRST
- [Proofview.V82.tactic assumption;
- Tacticals.New.tclTHEN (Proofview.V82.tactic (apply sym)) (Proofview.V82.tactic assumption);
+ [assumption;
+ Tacticals.New.tclTHEN (Proofview.V82.tactic (apply sym)) assumption;
try_prove_eq
]
]
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index f81698370..ad7654374 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -29,7 +29,7 @@ val h_intro_move : Id.t option -> Id.t move_location -> unit Proofview.tact
val h_intro : Id.t -> unit Proofview.tactic
val h_intros_until : quantified_hypothesis -> unit Proofview.tactic
-val h_assumption : tactic
+val h_assumption : unit Proofview.tactic
val h_exact : constr -> tactic
val h_exact_no_check : constr -> tactic
val h_vm_cast_no_check : constr -> tactic
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index f40ec7659..337ae5241 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1835,7 +1835,7 @@ let setoid_symmetry_in id =
let new_hyp = it_mkProd_or_LetIn new_hyp' binders in
Tacticals.New.tclTHENS (Proofview.V82.tactic (Tactics.cut new_hyp))
[ Proofview.V82.tactic (intro_replacing id);
- Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Proofview.V82.tactic (Tactics.assumption) ] ]
+ Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Tactics.assumption ] ]
end
let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 34314088c..248a5d36b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1756,7 +1756,7 @@ and interp_atomic ist tac =
let mloc = Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) gl in
h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
end
- | TacAssumption -> Proofview.V82.tactic h_assumption
+ | TacAssumption -> h_assumption
| TacExact c ->
Proofview.V82.tactic begin fun gl ->
let (sigma,c_interp) = pf_interp_casted_constr ist gl c in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0bf295b3c..2f52c8b7a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1166,19 +1166,36 @@ let exact_proof c gl =
let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
in refine_no_check c gl
-let (assumption : tactic) = fun gl ->
- let concl = pf_concl gl in
- let hyps = pf_hyps gl in
- let rec arec only_eq = function
- | [] ->
- if only_eq then arec false hyps else error "No such assumption."
- | (id,c,t)::rest ->
- if (only_eq && eq_constr t concl)
- || (not only_eq && pf_conv_x_leq gl t concl)
- then refine_no_check (mkVar id) gl
- else arec only_eq rest
+let tclZEROMSG msg =
+ Proofview.tclZERO (UserError ("", msg))
+
+let assumption =
+ let rec arec gl only_eq = function
+ | [] ->
+ if only_eq then
+ let hyps = Proofview.Goal.hyps gl in
+ arec gl false hyps
+ else tclZEROMSG (str "No such assumption.")
+ | (id, c, t)::rest ->
+ let concl = Proofview.Goal.concl gl in
+ let is_same_type =
+ if only_eq then eq_constr t concl
+ else
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ is_conv_leq env sigma t concl
+ in
+ if is_same_type then
+ let c = Goal.Refinable.make (fun _ -> Goal.return (mkVar id)) in
+ let r = Goal.bind c Goal.refine in
+ Proofview.tclSENSITIVE r
+ else arec gl only_eq rest
+ in
+ let assumption_tac gl =
+ let hyps = Proofview.Goal.hyps gl in
+ arec gl true hyps
in
- arec true hyps
+ Proofview.Goal.enter assumption_tac
(*****************************************************************)
(* Modification of a local context *)
@@ -3688,7 +3705,7 @@ let symmetry_in id =
| HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
Tacticals.New.tclTHENS (Proofview.V82.tactic (cut (it_mkProd_or_LetIn symccl sign)))
[ Proofview.V82.tactic (intro_replacing id);
- Tacticals.New.tclTHENLIST [ intros; symmetry; Proofview.V82.tactic (apply (mkVar id)); Proofview.V82.tactic assumption ] ]
+ Tacticals.New.tclTHENLIST [ intros; symmetry; Proofview.V82.tactic (apply (mkVar id)); assumption ] ]
end
begin function
| NoEquationFound -> Hook.get forward_setoid_symmetry_in id
@@ -3739,7 +3756,7 @@ let prove_transitivity hdcncl eq_kind t =
(Tacticals.New.tclTHENLIST
[ Tacticals.New.tclDO 2 intro;
Tacticals.New.onLastHyp simplest_case;
- Proofview.V82.tactic assumption ]))
+ assumption ]))
end
let transitivity_red allowred t =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index fc4c780fe..c3df47215 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -120,7 +120,7 @@ val intros_pattern :
(** {6 Exact tactics. } *)
-val assumption : tactic
+val assumption : unit Proofview.tactic
val exact_no_check : constr -> tactic
val vm_cast_no_check : constr -> tactic
val exact_check : constr -> tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 19:32:54 +0000