Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq et Injection

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2754 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 10 insertions, 9 deletions

diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index b9c6bbef8..4752b8ed7 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -111,7 +111,7 @@ let diseqCase =
   (tclTHEN  red_in_concl
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (h_simplest_apply (mkVar diseq))
-  (tclTHEN  (Extratactics.h_injHyp absurd)
+  (tclTHEN  (Extratactics.h_injHyp (Rawterm.NamedHyp absurd))
             full_trivial))))))
 
 let solveArg a1 a2 tac  g = 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 346b9dccb..8bebda9a3 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -802,7 +802,7 @@ let inj id gls =
 	    
 let injClause = function
   | None -> onNegatedEquality inj
-  | Some id -> inj id
+  | Some id -> try_intros_until inj id
 
 let injConcl gls  = injClause None gls
 let injHyp id gls = injClause (Some id) gls
@@ -865,7 +865,7 @@ let decompEq = decompEqThen (fun x -> tclIDTAC)
 
 let dEqThen ntac = function
   | None -> onNegatedEquality (decompEqThen ntac)
-  | Some id -> decompEqThen ntac id
+  | Some id -> try_intros_until (decompEqThen ntac) id
 
 let dEq = dEqThen (fun x -> tclIDTAC)
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 47ec78374..b9591189a 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -71,10 +71,10 @@ val discrHyp     : identifier -> tactic
 val discrEverywhere     : tactic
 val discr_tac    : identifier option -> tactic
 val inj          : identifier -> tactic
-val injClause    : clause -> tactic
+val injClause    : quantified_hypothesis option -> tactic
 
-val dEq : clause -> tactic
-val dEqThen : (int -> tactic) -> clause -> tactic
+val dEq : quantified_hypothesis option -> tactic
+val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic
 
 val make_iterated_tuple : 
   env -> evar_map -> (constr * constr) -> (constr * constr) 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 8ff06745f..0de8e2963 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -39,7 +39,7 @@ TACTIC EXTEND ReplaceIn
 END
 
 TACTIC EXTEND DEq
-  [ "Simplify_eq" ident_opt(h) ] -> [ dEq h ]
+  [ "Simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ]
 END
 
 TACTIC EXTEND Discriminate
@@ -49,7 +49,7 @@ END
 let h_discrHyp id = h_discriminate (Some id)
 
 TACTIC EXTEND Injection
-  [ "Injection" ident_opt(h) ] -> [ injClause h ]
+  [ "Injection" quantified_hypothesis_opt(h) ] -> [ injClause h ]
 END
 
 let h_injHyp id = h_injection (Some id)
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 0e178b52b..da842a438 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -11,9 +11,10 @@
 open Names
 open Term
 open Proof_type
+open Rawterm
 
 val h_discrHyp : identifier -> tactic
-val h_injHyp : identifier -> tactic
+val h_injHyp : quantified_hypothesis -> tactic
 val h_rewriteLR : constr -> tactic
 
 val refine_tac : Genarg.open_constr -> tactic