Fixes in generalize_eqs/dependent induction to allow the user to specify

generalized variables himself.


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

6 files changed, 45 insertions, 38 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 19ce087113..a2dc8a5058 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -501,9 +501,16 @@ END
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as 
   defined by Conor McBride *)
 TACTIC EXTEND generalize_eqs
-| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize id ]
+| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:false ]
+END
+TACTIC EXTEND generalize_eqs_vars
+| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:true ]
 END
 
 TACTIC EXTEND conv
 | ["conv" constr(x) constr(y) ] -> [ conv x y ]
 END
+
+TACTIC EXTEND resolve_classes
+| ["resolve_classes" ] -> [ resolve_classes ]
+END
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 586283d5a3..cb2acc9bd5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1972,29 +1972,23 @@ let abstract_args gl id =
 	       dep, succ (List.length ctx), vars)
     | _ -> None
 
-let abstract_generalize id gl =
+let abstract_generalize id ?(generalize_vars=true) gl =
   Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
-(*   let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string "Coq.Logic.JMeq")) in *)
-(*   Library.require_library [qualid] None; *)
   let oldid = pf_get_new_id id gl in
   let newc = abstract_args gl id in
     match newc with
       | None -> tclIDTAC gl
       | Some (newc, dep, n, vars) -> 
-	  if dep then
-	    tclTHENLIST [refine newc;
-			 rename_hyp [(id, oldid)];
-			 tclDO n intro; 
-			 generalize_dep (mkVar oldid);
-			 tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars]
-	      gl
-	  else
-	    tclTHENLIST [refine newc;
-			 clear [id];
-			 tclDO n intro; 
-			 tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars]
-	      gl
-
+	  let tac =
+	    if dep then
+	      tclTHENLIST [refine newc; rename_hyp [(id, oldid)]; tclDO n intro; 
+			   generalize_dep (mkVar oldid)]	      
+	    else
+	      tclTHENLIST [refine newc; clear [id]; tclDO n intro]
+	  in 
+	    if generalize_vars then
+	      tclTHEN tac (tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars) gl
+	    else tac gl
 
 let occur_rel n c = 
   let res = not (noccurn n c) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index cbf27b0320..9070e26179 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -340,12 +340,13 @@ val generalize_gen  : ((occurrences * constr) * name) list -> tactic
 val generalize_dep  : constr  -> tactic
 
 val conv            : constr -> constr -> tactic
+val resolve_classes : tactic
 
 val tclABSTRACT : identifier option -> tactic -> tactic
 
 val admit_as_an_axiom : tactic
 
-val abstract_generalize : identifier -> tactic
+val abstract_generalize : identifier -> ?generalize_vars:bool -> tactic
 
 val register_general_multi_rewrite : 
   (bool -> evars_flag -> constr with_ebindings -> clause -> tactic) -> unit
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 89e44c9bc4..cd30d77ca7 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -235,30 +235,43 @@ Ltac simpl_depind := subst* ; autoinjections ; try discriminates ;
    and starts a dependent induction using this tactic. *)
 
 Ltac do_depind tac H :=
+  generalize_eqs_vars H ; tac H ; repeat progress simpl_depind.
+
+(** A variant where generalized variables should be given by the user. *)
+
+Ltac do_depind' tac H :=
   generalize_eqs H ; tac H ; repeat progress simpl_depind.
 
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. *)
 
 Tactic Notation "dependent" "destruction" ident(H) := 
-  do_depind ltac:(fun H => destruct H ; intros) H ; subst*.
+  do_depind ltac:(fun hyp => destruct hyp ; intros) H ; subst*.
 
 Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
-  do_depind ltac:(fun H => destruct H using c ; intros) H.
+  do_depind ltac:(fun hyp => destruct hyp using c ; intros) H.
+
+(** This tactic also generalizes the goal by the given variables before the induction. *)
+
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := 
+  do_depind' ltac:(fun hyp => revert l ; destruct hyp ; intros) H.
+
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+  do_depind' ltac:(fun hyp => revert l ; destruct hyp using c ; intros) H.
 
 (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by 
    writting another wrapper calling do_depind. *)
 
 Tactic Notation "dependent" "induction" ident(H) := 
-  do_depind ltac:(fun H => induction H ; intros) H.
+  do_depind ltac:(fun hyp => induction hyp ; intros) H.
 
 Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := 
-  do_depind ltac:(fun H => induction H using c ; intros) H.
+  do_depind ltac:(fun hyp => induction hyp using c ; intros) H.
 
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
-  do_depind ltac:(fun H => generalize l ; clear l ; induction H ; intros) H.
+  do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp ; intros) H.
 
 Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
-  do_depind ltac:(fun H => generalize l ; clear l ; induction H using c ; intros) H.
+  do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c ; intros) H.
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 45e965142d..d7535c323c 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -77,10 +77,10 @@ Ltac clear_dup :=
   match goal with 
     | [ H : ?X |- _ ] => 
       match goal with
-        | [ H' : X |- _ ] =>
-          match H' with
-            | H => fail 2 
-            | _ => clear H' || clear H
+        | [ H' : ?Y |- _ ] =>
+          match H with
+            | H' => fail 2
+            | _ => conv X Y ; (clear H' || clear H)
           end
       end
   end.
@@ -158,14 +158,6 @@ Ltac autoinjection :=
   let tac H := progress (inversion H ; subst ; clear_dups) ; clear H in
     match goal with
       | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
-      | [ H : ?f ?a ?b = ?f' ?a' ?b'  |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g'  |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H
-      | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H
     end.
 
 Ltac autoinjections := repeat autoinjection.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a674bc3b78..ae91628600 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -825,7 +825,7 @@ let _ =
 let _ =
   declare_bool_option 
     { optsync  = true;
-      optname  = "implicit arguments defensive printing";
+      optname  = "implicit status of reversible patterns";
       optkey   = (TertiaryTable ("Reversible","Pattern","Implicit"));
       optread  = Impargs.is_reversible_pattern_implicit_args;
       optwrite = Impargs.make_reversible_pattern_implicit_args }