Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq et Injection

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

6 files changed, 14 insertions, 12 deletions

diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 4752b8ed7..8a13925c9 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -69,7 +69,8 @@ let mkBranches =
 
 let solveRightBranch  = 
   tclTHEN h_simplest_right
-    (tclTHEN (intro_force true) (onLastHyp Extratactics.h_discrHyp))
+    (tclTHEN (intro_force true)
+      (onLastHyp (fun id -> Extratactics.h_discrHyp (Rawterm.NamedHyp id))))
 
 let h_solveRightBranch =
   Refiner.abstract_extended_tactic "solveRightBranch" [] solveRightBranch
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8bebda9a3..2d68161c9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -551,7 +551,7 @@ let discrEverywhere =
 
 let discr_tac = function
   | None -> discrEverywhere
-  | Some id -> discr id
+  | Some id -> try_intros_until discr id
 
 let discrConcl gls  = discrClause None gls
 let discrHyp id gls = discrClause (Some id) gls
diff --git a/tactics/equality.mli b/tactics/equality.mli
index b9591189a..9e715751e 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -69,7 +69,7 @@ val discrClause  : clause -> tactic
 val discrConcl   : tactic
 val discrHyp     : identifier -> tactic
 val discrEverywhere     : tactic
-val discr_tac    : identifier option -> tactic
+val discr_tac    : quantified_hypothesis option -> tactic
 val inj          : identifier -> tactic
 val injClause    : quantified_hypothesis option -> tactic
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0de8e2963..3c6ea9ab3 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -43,7 +43,7 @@ TACTIC EXTEND DEq
 END
 
 TACTIC EXTEND Discriminate
-  [ "Discriminate" ident_opt(h) ] -> [ discr_tac h ]
+  [ "Discriminate" quantified_hypothesis_opt(h) ] -> [ discr_tac h ]
 END
 
 let h_discrHyp id = h_discriminate (Some id)
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index da842a438..8f650c661 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -13,7 +13,7 @@ open Term
 open Proof_type
 open Rawterm
 
-val h_discrHyp : identifier -> tactic
+val h_discrHyp : quantified_hypothesis -> tactic
 val h_injHyp : quantified_hypothesis -> tactic
 val h_rewriteLR : constr -> tactic
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5cd54c80e..4617ba354 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -33,6 +33,7 @@ open Elim
 open Equality
 open Typing
 open Pattern
+open Rawterm
 
 let collect_meta_variables c = 
   let rec collrec acc c = match kind_of_term c with
@@ -273,7 +274,7 @@ let projectAndApply thin id depids gls =
         let deq_trailer neqns =
           tclDO neqns
             (tclTHENSEQ [intro; tclTRY subst_hyp; trailer]) in 
-	(tclTHEN (dEqThen deq_trailer (Some id)) (clear [id])) gls
+	(tclTHEN (dEqThen deq_trailer (Some (NamedHyp id))) (clear [id])) gls
 
 (* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
    soi-meme (proposition de Valerie). *)
@@ -438,15 +439,15 @@ let com_of_id id =
 
 let inv k id = inv_gen false k NoDep id
 
-let half_inv_tac id = inv None (Rawterm.NamedHyp id)
-let inv_tac id = inv (Some false) (Rawterm.NamedHyp id)
-let inv_clear_tac id = inv (Some true) (Rawterm.NamedHyp id)
+let half_inv_tac id = inv None (NamedHyp id)
+let inv_tac id = inv (Some false) (NamedHyp id)
+let inv_clear_tac id = inv (Some true) (NamedHyp id)
 
 let dinv k c id = inv_gen false k (Dep c) id
 
-let half_dinv_tac id = dinv None None (Rawterm.NamedHyp id)
-let dinv_tac id = dinv (Some false) None (Rawterm.NamedHyp id)
-let dinv_clear_tac id = dinv (Some true) None (Rawterm.NamedHyp id)
+let half_dinv_tac id = dinv None None (NamedHyp id)
+let dinv_tac id = dinv (Some false) None (NamedHyp id)
+let dinv_clear_tac id = dinv (Some true) None (NamedHyp id)
 
 (* InvIn will bring the specified clauses into the conclusion, and then
  * perform inversion on the named hypothesis.  After, it will intro them