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

1 files changed, 13 insertions, 0 deletions

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index b7b62f394..c3870e6bd 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. *)