- 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

3 files changed, 94 insertions, 48 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ebf28e8eb..5ab401550 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -113,6 +113,13 @@ let guess_lpar_coloneq =
 let guess_lpar_colon =
   Gram.Entry.of_parser "guess_lpar_colon" (guess_lpar_ipat ":")
 
+let lookup_at_as_coma =
+  Gram.Entry.of_parser "lookup_at_as_coma"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+	| [("",(","|"at"|"as"))] -> ()
+	| _ -> raise Stream.Failure)
+
 open Constr
 open Prim
 open Tactic
@@ -286,7 +293,7 @@ GEXTEND Gram
       | IDENT "vm_compute" -> CbvVm
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
-      | IDENT "pattern"; pl = LIST1 pattern_occ SEP","-> Pattern pl ] ]
+      | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl ] ]
   ;
   (* This is [red_tactic] including possible extensions *)
   red_expr:
@@ -299,7 +306,7 @@ GEXTEND Gram
       | IDENT "vm_compute" -> CbvVm
       | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
-      | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl
+      | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl
       | s = IDENT -> ExtraRedExpr s ] ]
   ;
   hypident:
@@ -314,19 +321,27 @@ GEXTEND Gram
   hypident_occ:
     [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ]
   ;
-  clause:
-    [ [ "in"; "*"; occs=occs ->
+  in_clause:
+    [ [ "*"; occs=occs ->
           {onhyps=None; onconcl=true; concl_occs=occs}
-      | "in"; "*"; "|-"; (b,occs)=concl_occ ->
+      | "*"; "|-"; (b,occs)=concl_occ ->
           {onhyps=None; onconcl=b; concl_occs=occs}
-      | "in"; hl=LIST0 hypident_occ SEP","; "|-"; (b,occs)=concl_occ ->
+      | hl=LIST0 hypident_occ SEP","; "|-"; (b,occs)=concl_occ ->
           {onhyps=Some hl; onconcl=b; concl_occs=occs}
-      | "in"; hl=LIST0 hypident_occ SEP"," ->
-          {onhyps=Some hl; onconcl=false; concl_occs=[]}
-      | occs=occs ->
-	  {onhyps=Some[]; onconcl=true; concl_occs=occs}
-      | ->
-	  {onhyps=Some[]; onconcl=true; concl_occs=[]} ] ]
+      | hl=LIST0 hypident_occ SEP"," ->
+          {onhyps=Some hl; onconcl=false; concl_occs=[]} ] ]
+  ;
+  clause_dft_concl:
+    [ [ "in"; cl = in_clause -> cl
+      | occs=occs -> {onhyps=Some[]; onconcl=true; concl_occs=occs}
+      | -> {onhyps=Some[]; onconcl=true; concl_occs=[]} ] ]
+  ;
+  clause_dft_all:
+    [ [ "in"; cl = in_clause -> cl
+      | -> {onhyps=None; onconcl=true; concl_occs=[]} ] ]
+  ;
+  opt_clause:
+    [ [ "in"; cl = in_clause -> Some cl | -> None ] ]
   ;
   concl_occ:
     [ [ "*"; occs = occs -> (true,occs)
@@ -377,6 +392,9 @@ GEXTEND Gram
   with_names:
     [ [ "as"; ipat = simple_intropattern -> ipat | -> IntroAnonymous ] ]
   ;
+  as_name:
+    [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
+  ;
   by_tactic:
     [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
       | -> TacId [] ] ]
@@ -451,13 +469,15 @@ GEXTEND Gram
 	  TacMutualCofix (false,id,List.map mk_cofix_tac fd)
 
       | IDENT "pose"; (id,b) = bindings_with_parameters ->
-	  TacLetTac (Names.Name id,b,nowhere)
-      | IDENT "pose"; b = constr ->
-	  TacLetTac (Names.Anonymous,b,nowhere)
-      | IDENT "set"; (id,c) = bindings_with_parameters; p = clause ->
-	  TacLetTac (Names.Name id,c,p)
-      | IDENT "set"; c = constr; p = clause ->
-          TacLetTac (Names.Anonymous,c,p)
+	  TacLetTac (Names.Name id,b,nowhere,true)
+      | IDENT "pose"; b = constr; na = as_name ->
+	  TacLetTac (na,b,nowhere,true)
+      | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
+	  TacLetTac (Names.Name id,c,p,true)
+      | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
+          TacLetTac (na,c,p,true)
+      | IDENT "remember"; c = constr; na = as_name; p = clause_dft_all ->
+          TacLetTac (na,c,p,false)
 
       (* Begin compatibility *)
       | IDENT "assert"; id = lpar_id_coloneq; c = lconstr; ")" -> 
@@ -472,7 +492,14 @@ GEXTEND Gram
 	  TacAssert (None,ipat,c)
 
       | IDENT "cut"; c = constr -> TacCut c
-      | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc
+      | IDENT "generalize"; c = constr ->
+	  TacGeneralize [(([],c),Names.Anonymous)]
+      | IDENT "generalize"; c = constr; l = LIST1 constr ->
+          TacGeneralize (List.map (fun c -> (([],c),Names.Anonymous)) (c::l))
+      | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs; 
+          na = as_name; 
+          l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] ->
+          TacGeneralize (((nl,c),na)::l)
       | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c
 
       | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
@@ -483,17 +510,21 @@ GEXTEND Gram
       | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis ->
           TacSimpleInduction h
       | IDENT "induction"; lc = LIST1 induction_arg; ids = with_names; 
-	  el = OPT eliminator -> TacNewInduction (false,lc,el,ids)
+	  el = OPT eliminator; cl = opt_clause -> 
+	    TacNewInduction (false,lc,el,ids,cl)
       | IDENT "einduction"; lc = LIST1 induction_arg; ids = with_names; 
-	  el = OPT eliminator -> TacNewInduction (true,lc,el,ids)
+	  el = OPT eliminator; cl = opt_clause ->
+	    TacNewInduction (true,lc,el,ids,cl)
       | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
       | IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis ->
           TacSimpleDestruct h
       | IDENT "destruct"; lc = LIST1 induction_arg; ids = with_names; 
-	  el = OPT eliminator -> TacNewDestruct (false,lc,el,ids)
+	  el = OPT eliminator; cl = opt_clause ->
+	    TacNewDestruct (false,lc,el,ids,cl)
       | IDENT "edestruct"; lc = LIST1 induction_arg; ids = with_names; 
-	  el = OPT eliminator -> TacNewDestruct (true,lc,el,ids)
+	  el = OPT eliminator; cl = opt_clause ->
+	    TacNewDestruct (true,lc,el,ids,cl)
       | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
       | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
       | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr
@@ -544,14 +575,14 @@ GEXTEND Gram
 
       (* Equivalence relations *)
       | IDENT "reflexivity" -> TacReflexivity
-      | IDENT "symmetry"; cls = clause -> TacSymmetry cls
+      | IDENT "symmetry"; cl = clause_dft_concl -> TacSymmetry cl
       | IDENT "transitivity"; c = constr -> TacTransitivity c
 
       (* Equality and inversion *)
-      | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic ->
-	  TacRewrite (false,l,cl,t)
-      | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause; t=opt_by_tactic ->
-	  TacRewrite (true,l,cl,t)
+      | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; 
+	  cl = clause_dft_concl; t=opt_by_tactic -> TacRewrite (false,l,cl,t)
+      | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; 
+	  cl = clause_dft_concl; t=opt_by_tactic -> TacRewrite (true,l,cl,t)
       | IDENT "dependent"; k =
 	  [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
 	  | IDENT "inversion" -> FullInversion
@@ -573,9 +604,10 @@ GEXTEND Gram
 	    TacInversion (InversionUsing (c,cl), hyp)
 
       (* Conversion *)
-      | r = red_tactic; cl = clause -> TacReduce (r, cl)
+      | r = red_tactic; cl = clause_dft_concl -> TacReduce (r, cl)
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
-      | IDENT "change"; (oc,c) = conversion; cl = clause -> TacChange (oc,c,cl)
+      | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
+	  TacChange (oc,c,cl)
     ] ]
   ;
 END;;
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 57f1e80bd..c0dbc0eff 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -370,6 +370,13 @@ let pr_with_names = function
   | IntroAnonymous -> mt ()
   | ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
 
+let pr_as_name = function
+  | Anonymous -> mt ()
+  | Name id -> str "as " ++ pr_lident (dummy_loc,id)
+
+let pr_pose_as_style prc na c =
+  spc() ++ prc c ++ pr_as_name na
+
 let pr_pose prlc prc na c = match na with
   | Anonymous -> spc() ++ prc c
   | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c)
@@ -706,14 +713,18 @@ and pr_atom1 = function
              pr_assertion pr_lconstr pr_constr ipat c)
   | TacGeneralize l ->
       hov 1 (str "generalize" ++ spc () ++
-             prlist_with_sep spc pr_constr l)
+             prlist_with_sep pr_coma (fun (cl,na) -> 
+	       pr_with_occurrences pr_constr cl ++ pr_as_name na)
+	     l)
   | TacGeneralizeDep c ->
       hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
              pr_constrarg c)
-  | TacLetTac (na,c,cl) when cl = nowhere ->
+  | TacLetTac (na,c,cl,true) when cl = nowhere ->
       hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c)
-  | TacLetTac (na,c,cl) ->
-      hov 1 (str "set" ++ pr_pose pr_lconstr pr_constr na c ++
+  | TacLetTac (na,c,cl,b) ->
+      hov 1 ((if b then str "set" else str "remember") ++
+             (if b then pr_pose pr_lconstr else pr_pose_as_style)
+	        pr_constr na c ++
              pr_clauses pr_ident cl)
 (*  | TacInstantiate (n,c,ConclLocation ()) ->
       hov 1 (str "instantiate" ++ spc() ++
@@ -728,18 +739,20 @@ and pr_atom1 = function
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
       hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewInduction (ev,h,e,ids) ->
+  | TacNewInduction (ev,h,e,ids,cl) ->
       hov 1 (str (with_evars ev "induction") ++ spc () ++
 	     prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
 	     pr_with_names ids ++
-             pr_opt pr_eliminator e)
+             pr_opt pr_eliminator e ++
+             pr_opt_no_spc (pr_clauses pr_ident) cl)
   | TacSimpleDestruct h ->
       hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h)
-  | TacNewDestruct (ev,h,e,ids) ->
+  | TacNewDestruct (ev,h,e,ids,cl) ->
       hov 1 (str (with_evars ev "destruct") ++ spc () ++
              prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ 
 	     pr_with_names ids ++
-             pr_opt pr_eliminator e)
+             pr_opt pr_eliminator e ++
+             pr_opt_no_spc (pr_clauses pr_ident) cl)
   | TacDoubleInduction (h1,h2) ->
       hov 1
         (str "double induction" ++  
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a8ddfadb2..5c31fcee6 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -337,29 +337,30 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ 
 	      $mlexpr_of_constr c$ >>
   | Tacexpr.TacGeneralize cl ->
-      <:expr< Tacexpr.TacGeneralize $mlexpr_of_list mlexpr_of_constr cl$ >>
+      <:expr< Tacexpr.TacGeneralize
+	      $mlexpr_of_list 
+                (mlexpr_of_pair mlexpr_of_occ_constr mlexpr_of_name) cl$ >>
   | Tacexpr.TacGeneralizeDep c ->
       <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >>
-  | Tacexpr.TacLetTac (na,c,cl) ->
+  | Tacexpr.TacLetTac (na,c,cl,b) ->
       let na = mlexpr_of_name na in
       let cl = mlexpr_of_clause_pattern cl in
-      <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$ >>
+      <:expr< Tacexpr.TacLetTac $na$ $mlexpr_of_constr c$ $cl$
+	      $mlexpr_of_bool b$ >>
 
   (* Derived basic tactics *)
   | Tacexpr.TacSimpleInduction h ->
       <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$) >>
-  | Tacexpr.TacNewInduction (false,cl,cbo,ids) ->
+  | Tacexpr.TacNewInduction (false,cl,cbo,ids,cls) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
       let ids = mlexpr_of_intro_pattern ids in
-(*       let ids = mlexpr_of_option mlexpr_of_intro_pattern ids in *)
-(*       <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>> *)
-      <:expr< Tacexpr.TacNewInduction False $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$>>
+      <:expr< Tacexpr.TacNewInduction False $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >>
   | Tacexpr.TacSimpleDestruct h ->
       <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >>
-  | Tacexpr.TacNewDestruct (false,c,cbo,ids) ->
+  | Tacexpr.TacNewDestruct (false,c,cbo,ids,cls) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
       let ids = mlexpr_of_intro_pattern ids in
-      <:expr< Tacexpr.TacNewDestruct False $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ >>
+      <:expr< Tacexpr.TacNewDestruct False $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >>
 
   (* Context management *)
   | Tacexpr.TacClear (b,l) ->