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

3 files changed, 21 insertions, 19 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