From a8d50dd372fc9365d3f6f21551567f05937d93ef Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 5 Jan 2008 19:10:06 +0000
Subject: Fix a naming bug reported by Arnaud Spiwack, allow instance search to
 create evars and try to solve them too. Finally, rework tactics on setoids
 and design a saturating tactic to help solve goals on any setoid.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10428 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Tactics.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'theories/Program')

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index b7b62f394a..c3870e6bda 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -154,6 +154,19 @@ Ltac bang :=
 Tactic Notation "contradiction" "by" constr(t) := 
   let H := fresh in assert t as H by auto with * ; contradiction.
 
+(** A tactic that adds [H:=p:typeof(p)] to the context if no hypothesis of the same type appears in the goal.
+   Useful to do saturation using tactics. *)
+
+Ltac add_hypothesis H' p := 
+  match type of p with
+    ?X => 
+    match goal with 
+      | [ H : X |- _ ] => fail 1
+      | _ => set (H':=p) ; try (change p with H') ; clearbody H'
+    end
+  end.
+
+
 (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto with *]
    is overkill and slows things down, better rebind using [Obligations Tactic := tac] in this case, 
    possibly using [program_simplify] to use standard goal-cleaning tactics. *)
-- 
cgit v1.2.3