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

22 files changed, 256 insertions, 185 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index e90e7afaa2..8eda68e106 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -430,3 +430,29 @@ let congruence_tac depth l =
   tclORELSE 
     (tclTHEN (tclREPEAT introf) (cc_tactic depth l)) 
     cc_fail
+
+(* The [f_equal] tactic.
+
+   It mimics the use of lemmas [f_equal], [f_equal2], etc.
+   This isn't particularly related with congruence, apart from
+   the fact that congruence is called internally. 
+*)
+
+let f_equal gl = 
+  let cut_eq c1 c2 = 
+    tclTHENTRY
+      (Tactics.cut (mkApp (Lazy.force _eq, [| pf_type_of gl c1; c1; c2|])))
+      reflexivity
+  in 
+  try match kind_of_term (pf_concl gl) with 
+    | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> 
+	begin match kind_of_term t, kind_of_term t' with 
+	  | App (f,v), App (f',v') when Array.length v = Array.length v' ->
+	      let rec cuts i = 
+		if i < 0 then tclTRY (congruence_tac 1000 []) 
+		else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
+	      in cuts (Array.length v - 1) gl
+	  | _ -> tclIDTAC gl
+	end
+    | _ -> tclIDTAC gl
+  with Type_errors.TypeError _ -> tclIDTAC gl
diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli
index 0235252975..7cdd46ab4a 100644
--- a/contrib/cc/cctac.mli
+++ b/contrib/cc/cctac.mli
@@ -18,3 +18,5 @@ val cc_tactic : int -> constr list -> tactic
 val cc_fail : tactic
 
 val congruence_tac : int -> constr list -> tactic
+
+val f_equal : tactic
diff --git a/contrib/cc/g_congruence.ml4 b/contrib/cc/g_congruence.ml4
index 5b2cff9c27..f23ed49b6e 100644
--- a/contrib/cc/g_congruence.ml4
+++ b/contrib/cc/g_congruence.ml4
@@ -23,3 +23,7 @@ TACTIC EXTEND cc
  |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> 
    [ congruence_tac n l ]
 END
+
+TACTIC EXTEND f_equal
+ [ "f_equal" ] -> [ f_equal ]
+END
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index a0cbe22b36..16357fc472 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -340,7 +340,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacClear     _
     | TacClearBody _
     | TacMove      _
-    | TacRename    _ -> acc
+    | TacRename    _ 
+    | TacRevert    _ -> acc
 
     (* Constructors *)
     | TacLeft        cb
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c5a8c756a8..2219e327ca 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1187,6 +1187,7 @@ and xlate_tac =
        let idl' = List.map xlate_hyp idl in
        CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
     | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'"
+    | TacRevert _ -> xlate_error "TODO: revert"
     | (*For translating tactics/Inv.v *)
       TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
 	CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
@@ -1248,6 +1249,7 @@ and xlate_tac =
 	  (CT_formula_list
 	     (List.map xlate_formula
 		(out_gen (wit_list0 rawwit_constr) args)))
+    | TacExtend (_, "f_equal", _) -> xlate_error "TODO: f_equal"
     | TacExtend (_,id, l) ->
 	print_endline ("Extratactics : "^ id);
      CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 342b20cb57..e7ee8b1a4d 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -386,8 +386,8 @@ second-order pattern-matching problem into a first-order one.
     := {\term$_n$})} 
   
   This also provides {\tt apply} with values for instantiating
-  premises. But variables are referred by names and non dependent
-  products by order (see syntax in Section~\ref{Binding-list}).
+  premises. Here, variables are referred by names and non-dependent
+  products by increasing numbers (see syntax in Section~\ref{Binding-list}).
 
 \item {\tt eapply \term}\tacindex{eapply}\label{eapply}
   
@@ -558,44 +558,37 @@ in the list of subgoals remaining to prove.
 
 \item \texttt{pose proof {\term} as {\ident}}
 
-  This tactic behaves like \texttt{assert ({\ident:T} by exact {\term}} where
+  This tactic behaves like \texttt{assert ({\ident:T}) by exact {\term}} where
   \texttt{T} is the type of {\term}. 
 
-\end{Variants}
+\item {\tt specialize ({\ident} \term$_1$ {\ldots} \term$_n$)} \\
+      {\tt specialize {\ident} with \bindinglist}
+
+      The tactic {\tt specialize} works on local hypothesis \ident.
+      The premises of this hypothesis (either universal
+      quantifications or non-dependent implications) are instantiated
+      by concrete terms coming either from arguments \term$_1$
+      $\ldots$ \term$n$ or from a bindings list (see
+      Section~\ref{Binding-list} for more about bindings lists). In the
+      second form, all instantiation elements must be given, whereas
+      in the first form the application to \term$_1$ {\ldots}
+      \term$_n$ can be partial. The first form is equivalent to 
+      {\tt assert (\ident':=\ident \term$_1$ {\ldots} \term$_n$);
+           clear \ident; rename \ident' into \ident}. 
+
+      The name {\ident} can also refer to a global lemma or
+      hypothesis. In this case, for compatibility reasons, the
+      behavior of {\tt specialize} is close to the one of {\tt
+        generalize}: the instantiated statement becomes an additional 
+      premise of the goal. 
+
+%% Moreover, the old syntax allows the use of a number after {\tt specialize} 
+%% for controlling the number of premises to instantiate. Giving this 
+%% number should not be mandatory anymore (automatic detection of how
+%% many premises can be eaten without leaving meta-variables). Hence 
+%% no documentation for this integer optional argument of specialize
 
-% PAS CLAIR;
-% DEVRAIT AU MOINS FAIRE UN INTRO;
-% DEVRAIT ETRE REMPLACE PAR UN LET;
-% MESSAGE D'ERREUR STUPIDE
-% POURQUOI Specialize trans_equal ECHOUE ?
-%\begin{Variants}
-%\item {\tt Specialize \term} 
-%   \tacindex{Specialize} \\
-%   The argument {\tt t} should be a well-typed
-%   term of type {\tt T}.  This tactics is to make a cut of a
-%   proposition when you have already the proof of this proposition
-%   (for example it is a theorem applied to variables of local
-%   context). It is equivalent to {\tt Assert T. exact t}.
-%
-%\item {\tt Specialize {\term} with \vref$_1$ := {\term$_1$} \dots
-%    \vref$_n$ := \term$_n$}
-%  \tacindex{Specialize \dots\ with} \\ 
-%  It is to provide the tactic with some explicit values to instantiate
-%  premises of {\term} (see Section~\ref{Binding-list}).
-%  Some other premises are inferred using type information and
-%  unification. The resulting well-formed 
-%  term being {\tt (\term~\term'$_1$\dots\term'$_k$)}
-%  this tactic behaves as is used as 
-%  {\tt Specialize (\term~\term'$_1$\dots\term'$_k$)} \\ 
-%
-%  \ErrMsg {\tt Metavariable wasn't in the metamap} \\ 
-%  Arises when the information provided in the bindings list is not
-%  sufficient.
-%\item {\tt Specialize {\num} {\term} with \vref$_1$ := {\term$_1$} \dots\ 
-% \vref$_n$:= \term$_n$}\\ 
-%  The behavior is the same as before but only \num\ premises of 
-%  \term\ will be kept.
-%\end{Variants}
+\end{Variants}
 
 \subsection{{\tt apply {\term} in {\ident}}
 \tacindex{apply {\ldots} in}}
@@ -674,9 +667,11 @@ to $T$.
   This generalizes {\term} but also {\em all} hypotheses which depend
   on {\term}. It clears the generalized hypotheses.
 
-\item {\tt revert \term$_1$ \dots\ \term$_n$}\tacindex{revert}
+\item {\tt revert \ident$_1$ \dots\ \ident$_n$}\tacindex{revert}
  
-  This is equivalent to a {\tt generalize} followed by a {\tt clear}.
+  This is equivalent to a {\tt generalize} followed by a {\tt clear}
+  on the given hypotheses. This tactic can be seem as reciprocal to 
+  {\tt intros}. 
 
 \end{Variants}
 
@@ -795,14 +790,34 @@ the local context.
 
 This tactic applies to any goal. The {\tt contradiction} tactic
 attempts to find in the current context (after all {\tt intros}) one
-which is equivalent to {\tt False}. It permits to prune irrelevant
-cases.  This tactic is a macro for the tactics sequence {\tt intros;
-  elimtype False; assumption}.
+hypothesis which is equivalent to {\tt False}. It permits to prune 
+irrelevant cases. This tactic is a macro for the tactics sequence 
+{\tt intros; elimtype False; assumption}. 
 
 \begin{ErrMsgs}
 \item \errindex{No such assumption}
 \end{ErrMsgs}
 
+\begin{Variants}
+\item {\tt contradiction \ident}
+
+The proof of {\tt False} is searched in the hypothesis named \ident.
+\end{Variants}
+
+\subsection {\tt contradict \ident}
+\label{contradict}
+\tacindex{contradict}
+
+This tactic allows to manipulate negated hypothesis and goals. The
+name \ident\ should correspond to an hypothesis. With 
+{\tt contradict H}, the current goal and context is transformed in
+the following way: 
+\begin{itemize}
+\item  {\tt H:$\neg$A $\vd$  B} \ becomes \ {\tt $\vd$ A}
+\item  {\tt H:$\neg$A $\vd$ $\neg$B} \  becomes \ {\tt H: B $\vd$  A }
+\item  {\tt H: A $\vd$  B} \ becomes \ {\tt $\vd$ $\neg$A}
+\item  {\tt H: A $\vd$ $\neg$B} \ becomes \ {\tt H: B $\vd$ $\neg$A}
+\end{itemize}
 
 \section{Conversion tactics
 \index{Conversion tactics}
@@ -1294,12 +1309,13 @@ and {\tt induction {\term} as {\intropattern}}.
 
   \ErrMsg \errindex{Not the right number of dependent arguments}
 
-\item{\tt elim {\term} with {\vref$_1$} := {\term$_1$} \dots\ {\vref$_n$}
-    := {\term$_n$}} 
+\item{\tt elim {\term} with ({\vref$_1$} := {\term$_1$}) \dots\ ({\vref$_n$}
+    := {\term$_n$}}) 
   
-  Provides also {\tt elim} with values for instantiating premises by
-  associating explicitly variables (or non dependent products) with
-  their intended instance.
+  Also provides {\tt elim} with values for instantiating premises by
+  associating explicitly variables (or non-dependent products) with
+  their intended instance (see \ref{Binding-list} for more details
+  about bindings list). 
 
 \item{\tt elim {\term$_1$} using {\term$_2$}}
 \tacindex{elim \dots\ using} 
@@ -1978,10 +1994,6 @@ subgoals $f=f'$ and $a_1=a'_1$ and so on up to $a_n=a'_n$. Amongst
 these subgoals, the simple ones (e.g. provable by
 reflexivity or congruence) are automatically solved by {\tt f\_equal}.
 
-\Rem {\tt f\_equal} currently handles goals with only up to 5 arguments
-(i.e. $n\leq 5$). 
-
-
 
 \section{Equality and inductive sets}
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 96db00e3e4..b076220b45 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -458,6 +458,7 @@ GEXTEND Gram
       | IDENT "move"; id1 = id_or_meta; IDENT "after"; id2 = id_or_meta -> 
 	  TacMove (true,id1,id2)
       | IDENT "rename"; l = LIST1 rename SEP "," -> TacRename l
+      | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l
 
       (* Constructors *)
       | IDENT "left"; bl = with_bindings -> TacLeft bl
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 448b78e262..7775dc9816 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -787,6 +787,8 @@ and pr_atom1 = function
 	   (fun (i1,i2) -> 
 	      pr_ident i1 ++ spc () ++ str "into" ++ spc () ++ pr_ident i2)
 	   l)
+  | TacRevert l -> 
+      hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l) 
 
   (* Constructors *)
   | TacLeft l -> hov 1 (str "left" ++ pr_bindings l)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index f74413704b..5ddebf3c99 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -175,6 +175,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacClearBody of 'id list
   | TacMove of bool * 'id * 'id
   | TacRename of ('id *'id) list
+  | TacRevert of 'id list
 
   (* Constructors *)
   | TacLeft of 'constr bindings
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
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index f45b592af8..77bc295fd8 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -67,7 +67,7 @@ Proof with simpl in * ; auto ; simpl_depind.
     apply ax.
     
   destruct D...
-    narrow IHterm with G empty...
+    specialize (IHterm G empty)...
     apply weak...
 
     apply weak...
@@ -76,7 +76,7 @@ Proof with simpl in * ; auto ; simpl_depind.
     apply weak ; apply abs ; apply H.
 
     apply abs...
-    narrow IHterm with G0 (D, t, tau)...
+    specialize (IHterm G0 (D, t, tau))...
 
   apply app with tau...
 Qed.
@@ -97,7 +97,7 @@ Proof with simpl in * ; simpl_depind ; auto.
     apply weak...
 
   apply abs...
-  narrow IHterm with G0 (D, tau)...
+  specialize (IHterm G0 (D, tau))...
 
   eapply app with tau...
 Save.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
new file mode 100644
index 0000000000..4929ae4c0c
--- /dev/null
+++ b/test-suite/success/specialize.v
@@ -0,0 +1,48 @@
+
+Goal forall a b c : nat,  a = b -> b = c -> forall d, a+d=c+d.
+intros.
+
+(* "compatibility" mode: specializing a global name 
+   means a kind of generalize *)
+
+specialize trans_equal. intros _.
+specialize trans_equal with (1:=H)(2:=H0). intros _.
+specialize trans_equal with (x:=a)(y:=b)(z:=c). intros _.
+specialize trans_equal with (1:=H)(z:=c). intros _.
+specialize trans_equal with nat a b c. intros _.
+specialize (@trans_equal nat). intros _.
+specialize (@trans_equal _ a b c). intros _.
+specialize (trans_equal (x:=a)). intros _.
+specialize (trans_equal (x:=a)(y:=b)). intros _.
+specialize (trans_equal H H0). intros _.
+specialize (trans_equal H0 (z:=b)). intros _.
+
+(* local "in place" specialization *)
+assert (Eq:=trans_equal).
+
+specialize Eq.
+specialize Eq with (1:=H)(2:=H0). Undo.
+specialize Eq with (x:=a)(y:=b)(z:=c). Undo.
+specialize Eq with (1:=H)(z:=c). Undo.
+specialize Eq with nat a b c. Undo.
+specialize (Eq nat). Undo.
+specialize (Eq _ a b c). Undo.
+(* no implicit argument for Eq, hence no (Eq (x:=a)) *)
+specialize (Eq _ _ _ _ H H0). Undo.
+specialize (Eq _ _ _ b H0). Undo.
+
+(*
+(** strange behavior to inspect more precisely *)
+
+(* 1) proof aspect : let H:= ... in (fun H => ..) H
+    presque ok... *)
+
+(* 2) echoue moins lorsque zero premise de mangé *)
+specialize trans_equal with (1:=Eq).  (* mal typé !! *)
+
+(* 3) *)
+specialize trans_equal with _ a b c. intros _.
+(* Anomaly: Evar ?88 was not declared. Please report. *)
+*)
+
+Abort.
\ No newline at end of file
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 993f1ae79a..832829135b 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -584,8 +584,8 @@ Proof.
  rewrite in_find_iff, in_find_iff, H; intuition.
  rewrite find_mapsto_iff in H0,H1; congruence.
  destruct H.
- narrow H with y.
- narrow H0 with y.
+ specialize (H y).
+ specialize (H0 y).
  do 2 rewrite in_find_iff in H.
  generalize (find_mapsto_iff m y)(find_mapsto_iff m' y).
  do 2 destruct find; auto; intros.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index 1c8bac6d97..e8d639003b 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -387,19 +387,6 @@ the above form:
         end);
       cbv zeta beta in *.
 
-    (** If you have a negated goal and [H] is a negated
-        hypothesis, then [contra H] exchanges your goal and [H],
-        removing the negations.  (Just like [swap] but reuses
-        the same name. *)
-    Ltac contra H :=
-      let J := fresh in
-      unfold not;
-      unfold not in H;
-      intros J;
-      apply H;
-      clear H;
-      rename J into H.
-
     (** [decompose records] calls [decompose record H] on every
         relevant hypothesis [H]. *)
     Tactic Notation "decompose" "records" :=
@@ -704,15 +691,15 @@ the above form:
     unfold not in *;
     match goal with
     | H: (In ?x ?r) -> False |- (In ?x ?s) -> False =>
-      contra H; fsetdec_body
+      contradict H; fsetdec_body
     | H: (In ?x ?r) -> False |- (E.eq ?x ?y) -> False =>
-      contra H; fsetdec_body
+      contradict H; fsetdec_body
     | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
-      contra H; fsetdec_body
+      contradict H; fsetdec_body
     | H: ?P -> False |- ?Q -> False =>
       if prop (FSet_elt_Prop P) holds by
         (auto 100 with FSet_Prop)
-      then (contra H; fsetdec_body)
+      then (contradict H; fsetdec_body)
       else fsetdec_body
     | |- _ =>
       fsetdec_body
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index f61e9422e2..50653c4200 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -11,43 +11,43 @@
 Require Import Notations.
 Require Import Logic.
 
-(** Useful tactics *)
-
-(* A shorter name for generalize + clear, can be seen as an anti-intro *)
-
-Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l.
-
-(**************************************
- A tactic for proof by contradiction
-     with contradict H 
-         H: ~A |-   B      gives           |-   A
-         H: ~A |- ~ B     gives  H: B |-   A
-         H:   A |-   B      gives           |- ~ A
-         H:   A |-   B      gives           |- ~ A
-         H:   A |- ~ B     gives  H: A |- ~ A
-**************************************)
-
-Ltac contradict name := 
-     let term := type of name in (
-     match term with 
-       (~_) => 
-          match goal with 
-            |- ~ _  => let x := fresh in
-                     (intros x; case name; 
-                      generalize x; clear x name;
-                      intro name)
-          | |- _    => case name; clear name
-          end
-     | _ => 
-          match goal with 
-            |- ~ _  => let x := fresh in
-                    (intros x;  absurd term;
-                       [idtac | exact name]; generalize x; clear x name;
-                       intros name)
-          | |- _    => generalize name; absurd term;
-                       [idtac | exact name]; clear name
-          end
-     end).
+(** * Useful tactics *)
+
+(** A tactic for proof by contradiction. With contradict H, 
+    -   H:~A |-  B    gives       |-  A
+    -   H:~A |- ~B    gives  H: B |-  A
+    -   H: A |-  B    gives       |- ~A
+    -   H: A |- ~B    gives  H: B |- ~A
+   Moreover, negations may be in unfolded forms, 
+   and A or B may live in Type *)
+
+Ltac contradict H :=
+  let save tac H := let x:=fresh in intro x; tac H; rename x into H
+  in 
+  let negpos H := case H; clear H 
+  in 
+  let negneg H := save negpos H
+  in
+  let pospos H := 
+    let A := type of H in (elimtype False; revert H; try fold (~A))
+  in
+  let posneg H := save pospos H
+  in 
+  let neg H := match goal with 
+   | |- (~_) => negneg H
+   | |- (_->False) => negneg H
+   | |- _ => negpos H
+  end in 
+  let pos H := match goal with 
+   | |- (~_) => posneg H
+   | |- (_->False) => posneg H
+   | |- _ => pospos H
+  end in
+  match type of H with 
+   | (~_) => neg H
+   | (_->False) => neg H
+   | _ => pos H
+  end.
 
 (* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
 
@@ -55,62 +55,22 @@ Ltac swap H :=
   idtac "swap is OBSOLETE: use contradict instead.";
   intro; apply H; clear H.
 
-(* to contradict an hypothesis without copying its type. *)
+(* To contradict an hypothesis without copying its type. *)
 
-Ltac absurd_hyp h := 
+Ltac absurd_hyp H := 
   idtac "absurd_hyp is OBSOLETE: use contradict instead.";
-  let T := type of h in 
+  let T := type of H in 
   absurd T.
 
-(* A useful complement to contradict. Here t : ~ A where H : A. *)
+(* A useful complement to contradict. Here H : A and G allows to conclude ~A *)
 
-Ltac false_hyp h t := 
-  let T := type of h in absurd T; [ apply t | assumption ].
+Ltac false_hyp H G := 
+  let T := type of H in absurd T; [ apply G | assumption ].
 
 (* A case with no loss of information. *)
 
 Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
 
-(* A tactic for easing the use of lemmas f_equal, f_equal2, ... *)
-
-Ltac f_equal := 
-  let cg := try congruence in
-  let r := try reflexivity in 
-  match goal with 
-   | |- ?f ?a = ?f' ?a' => cut (a=a'); [cg|r]
-   | |- ?f ?a ?b = ?f' ?a' ?b' => 
-      cut (b=b');[cut (a=a');[cg|r]|r]
-   | |- ?f ?a ?b ?c = ?f' ?a' ?b' ?c'=> 
-      cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]
-   | |- ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d'=> 
-      cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]
-   | |- ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e'=> 
-      cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]|r]
-   | |- ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g' => 
-      cut (f=f');[cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]|r]|r]
-   | _ => idtac
-  end.
-
-(* Specializing universal hypothesis. 
-   The word "specialize" is already used for a not-documented-anymore 
-   tactic still used in some users contribs. Any idea for a better name?
-*)
-
-Tactic Notation "narrow" hyp(H) "with" constr(x) := 
- generalize (H x); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) := 
- generalize (H x y); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z):= 
- generalize (H x y z); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t):= 
- generalize (H x y z t); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t) constr(u):= 
- generalize (H x y z t u); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t) constr(u) constr(v) := 
- generalize (H x y z t u v); clear H; intro H.
-Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t) constr(u) constr(v) constr(w) := 
- generalize (H x y z t u v w); clear H; intro H.
-
 (* Rewriting in all hypothesis several times everywhere *)
 
 Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index f30c5b7630..6b02e8383f 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -162,7 +162,7 @@ Section Infinite_sets.
     generalize (H'3 x).
     intro H'4; lapply H'4; [ intro H'8; try exact H'8; clear H'4 | clear H'4 ];
       auto with sets.
-    specialize  5Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
+    specialize Im_inv with (U := U) (V := V) (X := A) (f := f) (y := x);
       intro H'11; lapply H'11; [ intro H'13; elim H'11; clear H'11 | clear H'11 ];
 	auto with sets.
     intros x1 H'4; try assumption.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 88cdabe3ff..ec44a6e582 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -87,7 +87,7 @@ Section Integers_sect.
     apply Totally_ordered_definition.
     simpl in |- *.
     intros H' x y H'0.
-    specialize  2le_or_lt with (n := x) (m := y); intro H'2; elim H'2.
+    elim le_or_lt with (n := x) (m := y).
     intro H'1; left; auto with sets arith.
     intro H'1; right.
     cut (y <= x); auto with sets arith.
@@ -142,8 +142,8 @@ Section Integers_sect.
     elim H'0; intros H'1 H'2.
     cut (In nat Integers (S x)).
     intro H'3.
-    specialize  1H'2 with (y := S x); intro H'4; lapply H'4;
-      [ intro H'5; clear H'4 | try assumption; clear H'4 ].
+    specialize H'2 with (y := S x); lapply H'2;
+      [ intro H'5; clear H'2 | try assumption; clear H'2 ].
     simpl in H'5.
     absurd (S x <= x); auto with arith.
     apply triv_nat.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index a7da7db9a4..d5257c12c1 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -140,10 +140,10 @@ intros U R H' x b H'0; elim H'0.
 intros x0 a H'1; exists a; auto with sets.
 intros x0 y z H'1 H'2 H'3 a H'4.
 red in H'.
-specialize  3H' with (x := x0) (a := a) (b := y); intro H'7; lapply H'7;
+specialize H' with (x := x0) (a := a) (b := y); lapply H'; 
  [ intro H'8; lapply H'8;
-    [ intro H'9; try exact H'9; clear H'8 H'7 | clear H'8 H'7 ]
- | clear H'7 ]; auto with sets.
+    [ intro H'9; try exact H'9; clear H'8 H' | clear H'8 H' ]
+ | clear H' ]; auto with sets.
 elim H'9.
 intros t H'5; elim H'5; intros H'6 H'7; try exact H'6; clear H'5.
 elim (H'3 t); auto with sets.