- 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

4 files changed, 22 insertions, 14 deletions

diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index be4f9c091..dd40c5cc3 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -295,16 +295,18 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacCut c -> depends_of_'constr c acc
     | TacAssert (taco, _, c) ->
 	Option.fold_right depends_of_'tac taco (depends_of_'constr c acc)
-    | TacGeneralize cl -> list_union_map depends_of_'constr cl acc
+    | TacGeneralize cl ->
+	list_union_map depends_of_'constr (List.map (fun ((_,c),_) -> c) cl)
+	acc
     | TacGeneralizeDep c -> depends_of_'constr c acc
-    | TacLetTac (_,c,_) -> depends_of_'constr c acc
+    | TacLetTac (_,c,_,_) -> depends_of_'constr c acc
 
     (* Derived basic tactics *)
     | TacSimpleInduction _
     | TacSimpleDestruct  _
     | TacDoubleInduction _ -> acc
-    | TacNewInduction (_, cwbial, cwbo, _)
-    | TacNewDestruct (_, cwbial, cwbo, _) ->
+    | TacNewInduction (_, cwbial, cwbo, _, _)
+    | TacNewDestruct (_, cwbial, cwbo, _, _) ->
 	list_union_map (depends_of_'a_induction_arg depends_of_'constr_with_bindings)
 	  cwbial
 	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index c16cde7d7..ac152f906 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -166,7 +166,7 @@ let make_pbp_atomic_tactic = function
       TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x]))
   | PbpGeneralize (h,args) ->
       let l = List.map make_pbp_pattern args in
-      TacAtom (zz, TacGeneralize [make_app (make_var h) l])
+      TacAtom (zz, TacGeneralize [([],make_app (make_var h) l),Anonymous])
   | PbpLeft -> TacAtom (zz, TacLeft (false,NoBindings))
   | PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
   | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 7f2019681..a2a504fb4 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1185,7 +1185,7 @@ let rec natural_ntree ig ntree =
 	  | TacFix (_,n) -> natural_fix ig lh g gs n ltree
 	  | TacSplit (_,_,NoBindings) -> natural_split ig lh g gs ge [] ltree
 	  | TacSplit(_,_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree
-	  | TacGeneralize l -> natural_generalize ig lh g gs ge (List.map snd l) ltree
+	  | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree
 	  | TacRight _ -> natural_right ig lh g gs ltree
 	  | TacLeft _ -> natural_left ig lh g gs ltree
 	  | (* "Simpl" *)TacReduce (r,cl)  ->
@@ -1652,7 +1652,7 @@ and natural_split ig lh g gs ge la ltree =
   | _ -> assert false
 and natural_generalize ig lh g gs ge la ltree =
   match la with
-    [arg] ->
+    [(_,(_,arg)),_] ->
       let _env= (gLOB ge) in
       let arg1= (*dbize env*) arg in
       let _type_arg=type_of (Global.env()) Evd.empty arg in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c2569a142..b041272c1 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1151,9 +1151,12 @@ and xlate_tac =
     | TacSpecialize (nopt, (c,sl)) ->
      CT_specialize (xlate_int_opt nopt, xlate_formula c, xlate_bindings sl)
     | TacGeneralize [] -> xlate_error ""
-    | TacGeneralize (first :: cl) ->
+    | TacGeneralize ((([],first),Anonymous) :: cl)
+	when List.for_all (fun ((o,_),na) -> o = [] & na = Anonymous) cl ->
      CT_generalize
-      (CT_formula_ne_list (xlate_formula first, List.map xlate_formula cl))
+      (CT_formula_ne_list (xlate_formula first, 
+                           List.map (fun ((_,c),_) -> xlate_formula c) cl))
+    | TacGeneralize _ -> xlate_error "TODO: Generalize at and as"
     | TacGeneralizeDep c ->
 	CT_generalize_dependent (xlate_formula c)
     | TacElimType c -> CT_elim_type (xlate_formula c)
@@ -1163,7 +1166,7 @@ and xlate_tac =
     | TacCase (false,(c1,sl)) ->
      CT_casetac (xlate_formula c1, xlate_bindings sl)
     | TacElim (true,_,_) | TacCase (true,_)
-    | TacNewDestruct (true,_,_,_) | TacNewInduction (true,_,_,_) ->
+    | TacNewDestruct (true,_,_,_,_) | TacNewInduction (true,_,_,_,_) ->
 	xlate_error "TODO: eelim, ecase, edestruct, einduction"
     | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
     | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
@@ -1207,24 +1210,27 @@ and xlate_tac =
 	CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
     | TacDAuto (a, b, _) ->
 	xlate_error "TODO: dauto using"
-    | TacNewDestruct(false,a,b,c) ->
+    | TacNewDestruct(false,a,b,c,None) ->
 	CT_new_destruct
 	  (List.map  xlate_int_or_constr a, xlate_using b, 
 	   xlate_with_names c)
-    | TacNewInduction(false,a,b,c) ->
+    | TacNewInduction(false,a,b,c,None) ->
 	CT_new_induction
 	  (List.map xlate_int_or_constr a, xlate_using b,
 	   xlate_with_names c)
+    | TacNewDestruct(false,a,b,c,_) -> xlate_error "TODO: destruct in"
+    | TacNewInduction(false,a,b,c,_) ->xlate_error "TODO: induction in"
     (*| TacInstantiate (a, b, cl) -> 
         CT_instantiate(CT_int a, xlate_formula b,
 		       assert false) *)
-    | TacLetTac (na, c, cl) when cl = nowhere -> 
+    | TacLetTac (na, c, cl, true) when cl = nowhere -> 
         CT_pose(xlate_id_opt_aux na, xlate_formula c)
-    | TacLetTac (na, c, cl) ->
+    | TacLetTac (na, c, cl, true) ->
         CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, 
 		  (* TODO LATER: This should be shared with Unfold,
 		     but the structures are different *)
 		  xlate_clause cl)
+    | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
     | TacAssert (None, IntroIdentifier id, c) -> 
         CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
     | TacAssert (None, IntroAnonymous, c) ->