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

12 files changed, 79 insertions, 151 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6cc7942f8e..c261d57e97 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -775,11 +775,12 @@ and xlate_red_tactic =
 and xlate_local_rec_tac = function 
  (* TODO LATER: local recursive tactics and global ones should be handled in
     the same manner *)
-  | ((_,x),(argl,tac)) ->
+  | ((_,x),Tacexp (TacFun (argl,tac))) ->
       let fst, rest = xlate_largs_to_id_opt argl in
 	CT_rec_tactic_fun(xlate_ident x,
 			  CT_id_opt_ne_list(fst, rest),
 			  xlate_tactic tac)
+  | _ -> xlate_error "TODO: more general argument of 'let rec in'"
 
 and xlate_tactic =
  function
@@ -837,36 +838,31 @@ and xlate_tactic =
    | TacMatchContext (false,true,rule1::rules) ->
          CT_match_context_reverse(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
-   | TacLetIn (l, t) ->
+   | TacLetIn (false, l, t) ->
        let cvt_clause =
          function
-             ((_,s),None,ConstrMayEval v) ->
+             ((_,s),ConstrMayEval v) ->
                  CT_let_clause(xlate_ident s,
 			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_DEF_BODY_to_LET_VALUE
                                (formula_to_def_body v))
-           | ((_,s),None,Tacexp t) -> 
+           | ((_,s),Tacexp t) -> 
                  CT_let_clause(xlate_ident s,
 			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_TACTIC_COM_to_LET_VALUE
                                (xlate_tactic t))
-           | ((_,s),None,t) -> 
+           | ((_,s),t) -> 
                  CT_let_clause(xlate_ident s,
 			       CT_coerce_NONE_to_TACTIC_OPT CT_none,
                                CT_coerce_TACTIC_COM_to_LET_VALUE
-                               (xlate_call_or_tacarg t))
-           | ((_,s),Some c,t) -> 
-	       CT_let_clause(xlate_ident s,
-			     CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic c),
-                               CT_coerce_TACTIC_COM_to_LET_VALUE
-				 (xlate_call_or_tacarg t)) in
+                               (xlate_call_or_tacarg t)) in
          let cl_l = List.map cvt_clause l in
          (match cl_l with
             | [] -> assert false 
             | fst::others ->
                 CT_let_ltac (CT_let_clauses(fst, others), mk_let_value t))
-   | TacLetRecIn([], _) -> xlate_error "recursive definition with no definition"
-   | TacLetRecIn(f1::l, t) -> 
+   | TacLetIn(true, [], _) -> xlate_error "recursive definition with no definition"
+   | TacLetIn(true, f1::l, t) -> 
        let tl =  CT_rec_tactic_fun_list
 		   (xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
        CT_rec_tactic_in(tl, xlate_tactic t)
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 2c6e0ebcd4..6c3b6337af 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -771,7 +771,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
   let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in
   Tacinterp.eval_tactic
     (TacLetIn
-      ([(dummy_loc,id_of_string"f"),None,Tacexp f],
+      (false,[(dummy_loc,id_of_string"f"),Tacexp f],
        ltac_lcall "f"
          [req;sth;ext;morph;th;cst_tac;pow_tac;
           lemma1;lemma2;pretac;posttac;lH;rl])) gl
@@ -1112,7 +1112,7 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl =
   let posttac = Tacexp(TacFun([None],e.field_post_tac)) in
   Tacinterp.eval_tactic
     (TacLetIn
-      ([(dummy_loc,id_of_string"f"),None,Tacexp f],
+      (false,[(dummy_loc,id_of_string"f"),Tacexp f],
        ltac_lcall "f"
         [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
          field_simpl_eq_in_ok;cond_ok;pretac;posttac;lH;rl])) gl
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index da39b1d3dd..00eb5c6d29 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1356,6 +1356,7 @@ Print Canonical Projections.
 \end{coq_example}
 
 \subsection{Implicit types of variables}
+\comindex{Implicit Types}
 
 It is possible to bind variable names to a given type (e.g. in a
 development using arithmetic, it may be convenient to bind the names
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index af9241e9dc..d9a1d47563 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -18,7 +18,7 @@ problems.
 \def\tacexprinf{\textrm{\textsl{tacexpr$_2$}}}
 \def\tacexprpref{\textrm{\textsl{tacexpr$_3$}}}
 \def\atom{\textrm{\textsl{atom}}}
-\def\recclause{\textrm{\textsl{rec\_clause}}}
+%%\def\recclause{\textrm{\textsl{rec\_clause}}}
 \def\letclause{\textrm{\textsl{let\_clause}}}
 \def\matchrule{\textrm{\textsl{match\_rule}}}
 \def\contextrule{\textrm{\textsl{context\_rule}}}
@@ -109,12 +109,9 @@ is understood as
 {\tacexprlow} & ::= &
 {\tt fun} \nelist{\name}{} {\tt =>} {\atom}\\
 & | &
-{\tt let} \nelist{\letclause}{\tt with} {\tt in}
+{\tt let} \zeroone{\tt rec} \nelist{\letclause}{\tt with} {\tt in}
 {\atom}\\
 & | &
-{\tt let rec} \nelist{\recclause}{\tt with} {\tt in}
-{\tacexpr}\\
-& | &
 {\tt match goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
 & | &
 {\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
@@ -168,8 +165,6 @@ is understood as
 \\
 \letclause & ::= & {\ident} \sequence{\name}{} {\tt :=} {\tacexpr}\\
 \\
-\recclause & ::= & {\ident} \nelist{\name}{} {\tt :=} {\tacexpr}\\
-\\
 \contextrule & ::= &
   \nelist{\contexthyps}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\
 & $|$ & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\
@@ -215,7 +210,7 @@ which is then applied to the current goal.
 
 There is a special case for {\tt match goal} expressions of which
 the clauses evaluate to tactics. Such expressions can only be used as
-end result of a tactic expression (never as argument of a local
+end result of a tactic expression (never as argument of a non recursive local
 definition or of an application).
 
 The rest of this section explains the semantics of every construction
@@ -444,8 +439,9 @@ for $i=1,...,n$. There is no dependencies between the {\tacexpr}$_i$
 and the {\ident}$_i$.
 
 Local definitions can be recursive by using {\tt let rec} instead of
-{\tt let}. Only functions can be defined by recursion, so at least one
-argument is required.
+{\tt let}. In this latter case, the definitions are evaluated lazily
+so that the {\tt rec} keyword can be used also in non recursive cases
+so as to avoid the eager evaluation of local definitions.
 
 \subsubsection{Application}
 
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 79e88f8cd8..87d45dc56e 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 7d83cffb69..67858b3c60 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 26dff3927a..b5ad753afc 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$
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index cb62c084d0..09d5c05165 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -22,6 +22,7 @@ type 'a or_metaid = AI of 'a | MetaId of loc * string
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag = bool      (* true = lazy             false = eager *)
 type evars_flag = bool     (* true = pose evars       false = fail on evars *)
+type rec_flag = bool       (* true = recursive        false = not recursive *)
 
 type raw_red_flag =
   | FBeta
@@ -217,8 +218,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
   | TacId of 'id message_token list
   | TacFail of int or_var * 'id message_token list
   | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
-  | TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
-  | TacLetIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
+  | TacLetIn of rec_flag * (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
   | TacMatchContext of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
   | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index b1eecef3f2..843554baee 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -300,7 +300,7 @@ let applyDestructor cls discard dd gls =
         | Some ((_,id),_), (Some x, tac) -> 
 	    let arg =
               ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in
-            TacLetIn ([(dummy_loc, x), None, arg], tac)
+            TacLetIn (false, [(dummy_loc, x), arg], tac)
         | None, (None, tac) -> tac
         | _, (Some _,_) -> error "Destructor expects an hypothesis"
         | _, (None,_) -> error "Destructor is for conclusion")
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 236b6f30f0..2112b91ece 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -82,7 +82,7 @@ type value =
   | VConstr of constr   (* includes idents known to be bound and references *)
   | VConstr_context of constr
   | VList of value list
-  | VRec of value ref
+  | VRec of (identifier*value) list ref * glob_tactic_expr
 
 let locate_tactic_call loc = function
   | VTactic (_,t) -> VTactic (loc,t)
@@ -308,7 +308,6 @@ let lookup_genarg_subst  id = let (_,_,f) = lookup_genarg id in f
 
 (* Dynamically check that an argument is a tactic, possibly unboxing VRec *)
 let coerce_to_tactic loc id = function
-  | VRec v -> !v
   | VTactic _ | VFun _ | VRTactic _ as a -> a
   | _ -> user_err_loc 
   (loc, "", str "variable " ++  pr_id id ++ str " should be bound to a tactic")
@@ -617,18 +616,9 @@ let rec intern_match_context_hyps sigma env lfun = function
   | [] -> lfun, [], []
 
 (* Utilities *)
-let extract_names lrc =
-  List.fold_right 
-    (fun ((loc,name),_) l ->
-      if List.mem name l then
-	user_err_loc
-	  (loc, "intern_tactic", str "This variable is bound several times");
-      name::l)
-    lrc []
-
 let extract_let_names lrc =
   List.fold_right 
-    (fun ((loc,name),_,_) l ->
+    (fun ((loc,name),_) l ->
       if List.mem name l then
 	user_err_loc
 	  (loc, "glob_tactic", str "This variable is bound several times");
@@ -777,19 +767,12 @@ and intern_tactic_seq ist = function
       let t = intern_atomic lf ist t in
       !lf, TacAtom (adjust_loc loc, t)
   | TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun)
-  | TacLetRecIn (lrc,u) ->
-      let names = extract_names lrc in
+  | TacLetIn (isrec,l,u) ->
       let (l1,l2) = ist.ltacvars in
-      let ist = { ist with ltacvars = (names@l1,l2) } in
-      let lrc = List.map (fun (n,b) -> (n,intern_tactic_fun ist b)) lrc in
-      ist.ltacvars, TacLetRecIn (lrc,intern_tactic ist u)
-  | TacLetIn (l,u) ->
-      let l = List.map
-        (fun (n,c,b) ->
-          (n,Option.map (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in
-      let (l1,l2) = ist.ltacvars in
-      let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in
-      ist.ltacvars, TacLetIn (l,intern_tactic ist' u)
+      let ist' = { ist with ltacvars = (extract_let_names l @ l1, l2) } in
+      let l = List.map (fun (n,b) -> 
+	  (n,intern_tacarg !strict_check (if isrec then ist' else ist) b)) l in
+      ist.ltacvars, TacLetIn (isrec,l,intern_tactic ist' u)
   | TacMatchContext (lz,lr,lmr) ->
       ist.ltacvars, TacMatchContext(lz,lr, intern_match_rule ist lmr)
   | TacMatch (lz,c,lmr) ->
@@ -1584,10 +1567,8 @@ let rec val_interp ist gl (tac:glob_tactic_expr) =
   let value_interp ist = match tac with
   (* Immediate evaluation *)
   | TacFun (it,body) -> VFun (ist.lfun,it,body)
-  | TacLetRecIn (lrc,u) -> letrec_interp ist gl lrc u
-  | TacLetIn (l,u) ->
-      let addlfun = interp_letin ist gl l in
-      val_interp { ist with lfun=addlfun@ist.lfun } gl u
+  | TacLetIn (true,l,u) -> interp_letrec ist gl l u
+  | TacLetIn (false,l,u) -> interp_letin ist gl l u
   | TacMatchContext (lz,lr,lmr) -> interp_match_context ist gl lz lr lmr 
   | TacMatch (lz,c,lmr) -> interp_match ist gl lz c lmr
   | TacArg a -> interp_tacarg ist gl a
@@ -1602,7 +1583,7 @@ let rec val_interp ist gl (tac:glob_tactic_expr) =
 
 and eval_tactic ist = function
   | TacAtom (loc,t) -> fun gl -> catch_error loc (interp_atomic ist gl t) gl
-  | TacFun _ | TacLetRecIn _ | TacLetIn _ -> assert false
+  | TacFun _ | TacLetIn _ -> assert false
   | TacMatchContext _ | TacMatch _ -> assert false
   | TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s)
   | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s)
@@ -1623,9 +1604,14 @@ and eval_tactic ist = function
   | TacComplete tac -> tclCOMPLETE (interp_tactic ist tac)
   | TacArg a -> assert false
 
+and force_vrec ist gl = function
+  | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} gl body
+  | v -> v
+
 and interp_ltac_reference isapplied mustbetac ist gl = function
   | ArgVar (loc,id) ->
       let v = List.assoc id ist.lfun in
+      let v = force_vrec ist gl v in
       if mustbetac then coerce_to_tactic loc id v else v
   | ArgArg (loc,r) ->
       let ids = extract_ids [] ist.lfun in
@@ -1714,47 +1700,20 @@ and eval_with_fail ist is_lazy goal tac =
     | FailError (lvl,s) ->
 	raise (FailError (lvl - 1, s))
 
-(* Interprets recursive expressions *)
-and letrec_interp ist gl lrc u =
-  let lref = Array.to_list (Array.make (List.length lrc) (ref VVoid)) in
-  let lenv =
-    List.fold_right2 (fun ((loc,name),_) vref l -> (name,VRec vref)::l)
-      lrc lref [] in
-  let lve = List.map (fun ((loc,name),(var,body)) ->
-                          (name,VFun(lenv@ist.lfun,var,body))) lrc in
-  begin
-    List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve;
-    val_interp { ist with lfun=lve@ist.lfun } gl u
-  end
+(* Interprets the clauses of a recursive LetIn *)
+and interp_letrec ist gl llc u =
+  let lref = ref ist.lfun in
+  let lve = list_map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg b))) llc in
+  lref := lve@ist.lfun;
+  let ist = { ist with lfun = lve@ist.lfun } in
+  val_interp ist gl u
 
 (* Interprets the clauses of a LetIn *)
-and interp_letin ist gl = function
-  | [] -> []
-  | ((loc,id),None,t)::tl -> 
-      let v = interp_tacarg ist gl t in
-      check_is_value v;
-      (id,v):: (interp_letin ist gl tl)
-  | ((loc,id),Some com,tce)::tl ->
-    let env = pf_env gl in
-    let typ = constr_of_value env (val_interp ist gl com)
-    and v = interp_tacarg ist gl tce in
-    let csr = 
-      try
-	constr_of_value env v
-      with Not_found ->
-      try
-	let t = tactic_of_value v in
-	let ndc = Environ.named_context_val env in
-	start_proof id (Local,Proof Lemma) ndc typ (fun _ _ -> ());
-	by t;
-	let (_,({const_entry_body = pft},_,_)) = cook_proof () in
-	delete_proof (dloc,id);
-        pft
-      with | NotTactic ->
-	delete_proof (dloc,id);
-	errorlabstrm "Tacinterp.interp_letin"
-          (str "Term or fully applied tactic expected in Let")
-    in (id,VConstr (mkCast (csr,DEFAULTcast, typ)))::(interp_letin ist gl tl)
+and interp_letin ist gl llc u =
+  let lve = list_map_left (fun ((_,id),body) ->
+    let v = interp_tacarg ist gl body in check_is_value v; (id,v)) llc in
+  let ist = { ist with lfun = lve@ist.lfun } in
+  val_interp ist gl u
 
 (* Interprets the Match Context expressions *)
 and interp_match_context ist g lz lr lmr =
@@ -2460,12 +2419,9 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t)
   | TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun)
-  | TacLetRecIn (lrc,u) ->
-      let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in
-      TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr))
-  | TacLetIn (l,u) ->
-      let l = List.map (fun (n,c,b) -> (n,Option.map (subst_tactic subst) c,subst_tacarg subst b)) l in
-      TacLetIn (l,subst_tactic subst u)
+  | TacLetIn (r,l,u) ->
+      let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in
+      TacLetIn (r,l,subst_tactic subst u)
   | TacMatchContext (lz,lr,lmr) ->
       TacMatchContext(lz,lr, subst_match_rule subst lmr)
   | TacMatch (lz,c,lmr) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3be4f0f137..39765526f0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -167,7 +167,7 @@ let reduct_in_concl (redfun,sty) gl =
 
 let reduct_in_hyp redfun ((_,id),where) gl =
   let (_,c, ty) = pf_get_hyp gl id in
-  let redfun' = (*under_casts*) (pf_reduce redfun gl) in
+  let redfun' = pf_reduce redfun gl in
   match c with
   | None -> 
       if where = InHypValueOnly then
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 880b5da11f..9dd7b273d6 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -198,3 +198,14 @@ Goal forall x : nat, x = 1 -> x + x + x = 3.
 intros x H.
 test x 2.
 Abort.
+
+(* Utilisation de let rec sans arguments *)
+
+Ltac is := 
+  let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in
+  i.
+
+Goal True -> True -> True.
+is.
+exact I.
+Abort.