f_equal, revert, specialize in ML, contradict in better Ltac (+doc)

 * "f_equal" is now a tactic in ML (placed alongside congruence since
   it uses it). Normally, it should be completely compatible with the
   former Ltac version, except that it doesn't suffer anymore from the
   "up to 5 args" earlier limitation.

 * "revert" also becomes an ML tactic. This doesn't bring any real 
   improvement, just some more uniformity with clear and generalize.  

 * The experimental "narrow" tactic is removed from Tactics.v, and 
   replaced by an evolution of the old & undocumented "specialize" 
   ML tactic: 
   - when specialize is called on an hyp H, the specialization is 
     now done in place on H. For instance "specialize (H t u v)"
     removes the three leading forall of H and intantiates them by 
     t u and v.
   - otherwise specialize still works as before (i.e. as a kind of 
     generalize).
   See the RefMan and test-suite/accept/specialize.v for more infos. 
   Btw, specialize can still accept an optional number for specifying 
   how many premises to instantiate. This number should normally 
   be useless now (some autodetection mecanism added). Hence this 
   feature is left undocumented. For the happy few still using 
   specialize in the old manner, beware of the slight incompatibities...

 * finally, "contradict" is left as Ltac in Tactics.v, but it has 
   now a better shape (accepts unfolded nots and/or things in Type), 
   and also some documentation in the RefMan



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

5 files changed, 46 insertions, 21 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index f5c54a5336..60f1ccf0ca 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -83,7 +83,7 @@ let h_new_induction ev c e idl =
 let h_new_destruct ev c e idl =
   abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl))
     (new_destruct ev c e idl)
-let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (new_hyp n d)
+let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (specialize n d)
 let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c)
 
 (* Context management *)
@@ -94,6 +94,7 @@ let h_move dep id1 id2 =
   abstract_tactic (TacMove (dep,id1,id2)) (move_hyp dep id1 id2)
 let h_rename l =
   abstract_tactic (TacRename l) (rename_hyp l)
+let h_revert l = abstract_tactic (TacRevert l) (revert l)
 
 (* Constructors *)
 let h_left l    = abstract_tactic (TacLeft l) (left_with_ebindings l)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 87232988b8..909d294cf6 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -76,7 +76,7 @@ val h_clear           : bool -> identifier list -> tactic
 val h_clear_body      : identifier list -> tactic
 val h_move            : bool -> identifier -> identifier -> tactic
 val h_rename          : (identifier*identifier) list -> tactic
-
+val h_revert          : identifier list -> tactic
 
 (* Constructors *)
 val h_constructor     : int -> open_constr bindings -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3245c31c7e..821586e7f0 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -718,6 +718,7 @@ let rec intern_atomic lf ist x =
       TacRename (List.map (fun (id1,id2) -> 
 			     intern_hyp_or_metaid ist id1, 
 			     intern_hyp_or_metaid ist id2) l)
+  | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l)
 	
   (* Constructors *)
   | TacLeft bl -> TacLeft (intern_bindings ist bl)
@@ -2079,6 +2080,7 @@ and interp_atomic ist gl = function
       h_rename (List.map (fun (id1,id2) -> 
 			    interp_hyp ist gl id1, 
 			    interp_fresh_ident ist gl (snd id2)) l)
+  | TacRevert l -> h_revert (interp_hyp_list ist gl l)
 
   (* Constructors *)
   | TacLeft bl -> h_left (interp_bindings ist gl bl)
@@ -2386,6 +2388,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacClearBody l as x -> x
   | TacMove (dep,id1,id2) as x -> x
   | TacRename l as x -> x
+  | TacRevert _ as x -> x
 
   (* Constructors *)
   | TacLeft bl -> TacLeft (subst_bindings subst bl)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6119185438..5f919a4dbe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -725,25 +725,41 @@ let rec intros_clearing = function
       tclTHENLIST
         [ intro; onLastHyp (fun id -> clear [id]); intros_clearing tl]
 
-(* Adding new hypotheses  *)
-
-let new_hyp mopt (c,lbind) g =
-  let clause  = make_clenv_binding g (c,pf_type_of g c) lbind in
-  let clause = clenv_unify_meta_types clause in
-  let (thd,tstack) = whd_stack (clenv_value clause) in
-  let nargs = List.length tstack in
-  let cut_pf = 
-    applist(thd, 
-            match mopt with
-	      | Some m -> if m < nargs then list_firstn m tstack else tstack
-	      | None   -> tstack)
+(* Modifying/Adding an hypothesis  *)
+
+let specialize mopt (c,lbind) g =
+  let evars, term = 
+    if lbind = NoBindings then None, c 
+    else 
+      let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
+      let clause = clenv_unify_meta_types clause in
+      let (thd,tstack) = whd_stack (clenv_value clause) in
+      let nargs = List.length tstack in
+      let tstack = match mopt with 
+	| Some m -> 
+	    if m < nargs then list_firstn m tstack else tstack
+	| None -> 
+	    let rec chk = function 
+	      | [] -> []
+	      | t::l -> if occur_meta t then [] else t :: chk l
+	    in chk tstack
+      in 
+      let term = applist(thd,tstack) in 
+      if occur_meta term then
+	errorlabstrm "" (str "Cannot infer an instance for " ++
+          pr_name (meta_name clause.evd (List.hd (collect_metas term))));
+      Some (evars_of clause.evd), term
   in
-  if occur_meta cut_pf then
-    errorlabstrm "" (str "Cannot infer an instance for " ++
-      pr_name (meta_name clause.evd (List.hd (collect_metas cut_pf))));
-  (tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.evd))
-               (cut (pf_type_of g cut_pf)))
-     ((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
+  tclTHEN 
+    (match evars with Some e -> tclEVARS e | _ -> tclIDTAC)
+    (match kind_of_term (fst (decompose_app c)) with 
+       | Var id when List.exists (fun (i,_,_)-> i=id) (pf_hyps g) ->
+	   let id' = fresh_id [] id g in 
+	   tclTHENS (internal_cut id' (pf_type_of g term))
+	     [ exact_no_check term; 
+	       tclTHEN (clear [id]) (rename_hyp [id',id]) ]
+       | _ -> tclTHENLAST (cut (pf_type_of g term)) (exact_no_check term))
+    g
 
 (* Keeping only a few hypotheses *)
 
@@ -1084,6 +1100,9 @@ let generalize lconstr gl =
   let newcl = List.fold_right (generalize_goal gl) lconstr (pf_concl gl) in
   apply_type newcl lconstr gl
 
+let revert hyps gl = 
+  tclTHEN (generalize (List.map mkVar hyps)) (clear hyps) gl
+
 (* Faudra-t-il une version avec plusieurs args de generalize_dep ?
 Cela peut-être troublant de faire "Generalize Dependent H n" dans
 "n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index eb62f602aa..3a3bf6de51 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -156,11 +156,13 @@ val clear         : identifier list -> tactic
 val clear_body    : identifier list -> tactic
 val keep          : identifier list -> tactic
 
-val new_hyp       : int option -> constr with_ebindings -> tactic
+val specialize    : int option -> constr with_ebindings -> tactic
 
 val move_hyp      : bool -> identifier -> identifier -> tactic
 val rename_hyp    : (identifier * identifier) list -> tactic
 
+val revert        : identifier list -> tactic
+
 (*s Resolution tactics. *)
 
 val apply_type : constr -> constr list -> tactic