diff options
| author | herbelin | 2008-02-01 08:55:51 +0000 |
|---|---|---|
| committer | herbelin | 2008-02-01 08:55:51 +0000 |
| commit | a502c83b5c9878ef30a8f25f945ff0ef7b70f0f6 (patch) | |
| tree | 78a20b6198ab1b96645a20cbf8648b28a8e4a52e /proofs | |
| parent | 4e4293dba98be63d44759f2a81c18ea7f1f01a08 (diff) | |
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
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |