- 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

2 files changed, 3 insertions, 2 deletions

diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index 71f483fb61..dae76f2dd9 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -317,7 +317,7 @@ let mkEq typ c1 c2 =
 let poseq_unsafe idunsafe cstr gl =
   let typ = Tacmach.pf_type_of gl cstr in
   tclTHEN
-    (Tactics.letin_tac true (Name idunsafe) cstr allClauses)
+    (Tactics.letin_tac None (Name idunsafe) cstr allClauses)
     (tclTHENFIRST 
       (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) 
       Tactics.reflexivity)
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index a071add636..a6cbb3211b 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -120,7 +120,8 @@ let functional_induction with_clean c princl pat =
 	 princ_infos
 	 args_as_induction_constr
 	 princ'
-	 pat)
+	 pat
+         None)
       subst_and_reduce
       g