Unification de TacLetRecIn et TacLetIn. En particulier, on peut

maintenant écrire des fonctions récursives qui n'ont pas l'apparence
d'être fonctionnelle. La sémantique reste toutefois différente. Par
exemple, dans

Ltac is := 
  let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in
  i.

l'évaluation de i est paresseuse, alors que dans une version non récursive

Ltac is := 
  let i := match goal with |- ?A -> ?B => intro | _ => idtac end in
  i.

l'évaluation de i est forte (et échoue sur le "match" qui n'est pas
autorisé à retourner une tactique).

(note: code mort dans tactics.ml en passant + indexation Implicit Type dans doc)


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

3 files changed, 16 insertions, 48 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 79e88f8cd..87d45dc56 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -20,19 +20,8 @@ open Pcoq
 open Prim
 open Tactic
 
-type let_clause_kind =
-  | LETTOPCLAUSE of Names.identifier * constr_expr
-  | LETCLAUSE of
-      (Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg)
-
 let fail_default_value = ArgArg 0
 
-let out_letin_clause loc = function
-  | LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error"))
-  | LETCLAUSE (id,c,d) -> (id,c,d)
-
-let make_letin_clause loc = List.map (out_letin_clause loc)
-
 let arg_of_expr = function
     TacArg a -> a
   | e -> Tacexp (e:raw_tactic_expr)
@@ -122,10 +111,9 @@ GEXTEND Gram
     [ RIGHTA
       [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" ->
           TacFun (it,body)
-      | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in";
-          body = tactic_expr LEVEL "5" -> TacLetRecIn (rcl,body)
-      | "let"; llc = LIST1 let_clause SEP "with"; "in";
-          u = tactic_expr LEVEL "5" -> TacLetIn (make_letin_clause loc llc,u)
+      | "let"; isrec = [IDENT "rec" -> true | -> false]; 
+          llc = LIST1 let_clause SEP "with"; "in";
+          body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body)
       | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ]
   ;
   (* Tactic arguments *)
@@ -173,12 +161,12 @@ GEXTEND Gram
   ;
   let_clause:
     [ [ id = identref; ":="; te = tactic_expr ->
-          LETCLAUSE (id, None, arg_of_expr te)
+         (id, arg_of_expr te)
       | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
-          LETCLAUSE (id, None, arg_of_expr (TacFun(args,te))) ] ]
+         (id, arg_of_expr (TacFun(args,te))) ] ]
   ;
   rec_clause:
-    [ [ name = identref; it = LIST1 input_fun; ":="; body = tactic_expr ->
+    [ [ name = identref; it = LIST0 input_fun; ":="; body = tactic_expr ->
           (name,(it,body)) ] ]
   ;
   match_pattern:
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 7d83cffb6..67858b3c6 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -473,29 +473,16 @@ let pr_funvar = function
   | None -> spc () ++ str "_"
   | Some id -> spc () ++ pr_id id
 
-let pr_let_clause k pr = function
-  | (id,None,t) ->
-      hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++
-             pr (TacArg t))
-  | (id,Some c,t) ->
-      hv 0 (str k ++ pr_lident id ++ str" :" ++ brk(1,2) ++
-      pr c ++
-      str " :=" ++ brk (1,1) ++ pr (TacArg t))
-
-let pr_let_clauses pr = function
+let pr_let_clause k pr (id,t) =
+  hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++ pr (TacArg t))
+
+let pr_let_clauses recflag pr = function
   | hd::tl ->
       hv 0
-        (pr_let_clause "let " pr hd ++
+        (pr_let_clause (if recflag then "let rec " else "let ") pr hd ++
          prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl)
   | [] -> anomaly "LetIn must declare at least one binding"
 
-let pr_rec_clause pr (id,(l,t)) =
-  hov 0
-    (pr_lident id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
-
-let pr_rec_clauses pr l = 
-  prlist_with_sep (fun () -> fnl () ++ str "with ") (pr_rec_clause pr) l
-
 let pr_seq_body pr tl =
   hv 0 (str "[ " ++
         prlist_with_sep (fun () -> spc () ++ str "| ") pr tl ++
@@ -858,15 +845,9 @@ let rec pr_tac inherited tac =
        (str "abstract (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () ++
         str "using " ++ pr_id s),
       labstract
-  | TacLetRecIn (l,t) -> 
-      hv 0
-        (str "let rec " ++ pr_rec_clauses (pr_tac ltop) l ++ str " in" ++
-         fnl () ++ pr_tac (llet,E) t),
-      llet
-  | TacLetIn (llc,u) ->
+  | TacLetIn (recflag,llc,u) ->
       v 0
-       (hv 0 (pr_let_clauses (pr_tac ltop) llc
-       ++ str " in") ++
+       (hv 0 (pr_let_clauses recflag (pr_tac ltop) llc ++ str " in") ++
        fnl () ++ pr_tac (llet,E) u),
       llet
   | TacMatch (lz,t,lrul) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 26dff3927..b5ad753af 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -448,13 +448,12 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
   | Tacexpr.TacRec (id,(idl,t)) -> TacRec (loc,(id,(idl,f t)))
   | Tacexpr.TacRecIn (l,t) -> TacRecIn(loc,List.map (fun (id,t) -> (id,f t)) l,f t)
 *)
-  | Tacexpr.TacLetIn (l,t) ->
+  | Tacexpr.TacLetIn (isrec,l,t) ->
       let f =
-	mlexpr_of_triple
+	mlexpr_of_pair
 	  (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_ident)
-	  (mlexpr_of_option mlexpr_of_tactic)
 	  mlexpr_of_tactic_arg in
-      <:expr< Tacexpr.TacLetIn $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >>
+      <:expr< Tacexpr.TacLetIn $mlexpr_of_bool isrec$ $mlexpr_of_list f l$ $mlexpr_of_tactic t$ >>
   | Tacexpr.TacMatch (lz,t,l) ->
       <:expr< Tacexpr.TacMatch
         $mlexpr_of_bool lz$