- Extension de "generalize" en "generalize c as id at occs".

- Ajout clause "in" à "remember" (et passage du code en ML).
- Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute
  aussi une égalité pour se souvenir du terme sur lequel l'induction
  ou l'analyse de cas s'applique.
- Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de
  Programs qui avait la sémantique de "pose proof" tandis que le nouveau
  a la même sémantique que "pose (id:=t)").
- Un peu de réorganisation, uniformisation de noms dans Arith, et
  ajout EqNat dans Arith.
- Documentation tactiques et notations de tactiques.



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

1 files changed, 12 insertions, 7 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 92ca06647..a6ae7240c 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -514,12 +514,14 @@ let compute_bl_tact ind lnamesparrec nparrec  =
                      new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn),
                                         Rawterm.NoBindings))]
                                 None
-                                Genarg.IntroAnonymous;
+                                Genarg.IntroAnonymous
+		                None;
                      intro_using freshm;
                      new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm),
                                     Rawterm.NoBindings))]
                                 None
-                                Genarg.IntroAnonymous;
+                                Genarg.IntroAnonymous
+		                None;
                      intro_using freshz;
                      intros;
                      tclTRY ( 
@@ -541,7 +543,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                                   None
                                   ( Genarg.IntroOrAndPattern [[
                                     Genarg.IntroIdentifier fresht;
-                                    Genarg.IntroIdentifier freshz]])) gl
+                                    Genarg.IntroIdentifier freshz]]) None) gl
                         ]);
 (*
   Ci a1 ... an = Ci b1 ... bn 
@@ -629,12 +631,14 @@ let compute_lb_tact ind lnamesparrec nparrec =
                      new_induct false [Tacexpr.ElimOnConstr 
                                     ((mkVar freshn),Rawterm.NoBindings)] 
                                 None
-                                Genarg.IntroAnonymous;
+                                Genarg.IntroAnonymous
+		                None;
                      intro_using freshm;
                      new_destruct false [Tacexpr.ElimOnConstr 
                                     ((mkVar freshm),Rawterm.NoBindings)]
                                 None
-                                Genarg.IntroAnonymous;
+                                Genarg.IntroAnonymous
+		                None;
                      intro_using freshz;
                      intros;
                      tclTRY ( 
@@ -748,7 +752,8 @@ let compute_dec_tact ind lnamesparrec nparrec =
                    (new_destruct false [Tacexpr.ElimOnConstr
                                   (eqbnm,Rawterm.NoBindings)]
                                 None
-                                Genarg.IntroAnonymous)
+                                Genarg.IntroAnonymous
+		                None)
                   Auto.default_auto
                 );
       Pfedit.by (
@@ -759,7 +764,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
                                 None
                                 (Genarg.IntroOrAndPattern [
                                     [Genarg.IntroAnonymous];
-                                    [Genarg.IntroIdentifier freshH2]]) 
+                                    [Genarg.IntroIdentifier freshH2]]) None
       );
       let arfresh = Array.of_list fresh_first_intros in
         let xargs = Array.sub arfresh 0 (2*nparrec) in