aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml22
-rw-r--r--contrib/setoid_ring/newring.ml44
-rw-r--r--doc/refman/RefMan-ext.tex1
-rw-r--r--doc/refman/RefMan-ltac.tex16
-rw-r--r--parsing/g_ltac.ml424
-rw-r--r--parsing/pptactic.ml33
-rw-r--r--parsing/q_coqast.ml47
-rw-r--r--proofs/tacexpr.ml4
-rw-r--r--tactics/dhyp.ml2
-rw-r--r--tactics/tacinterp.ml104
-rw-r--r--tactics/tactics.ml2
-rw-r--r--test-suite/success/ltac.v11
12 files changed, 79 insertions, 151 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6cc7942f8..c261d57e9 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 2c6e0ebcd..6c3b6337a 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 da39b1d3d..00eb5c6d2 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 af9241e9d..d9a1d4756 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 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$
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index cb62c084d..09d5c0516 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 b1eecef3f..843554bae 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 236b6f30f..2112b91ec 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 3be4f0f13..39765526f 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 880b5da11..9dd7b273d 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 23:05:03 +0000