diff options
| author | herbelin | 2008-02-01 10:21:54 +0000 |
|---|---|---|
| committer | herbelin | 2008-02-01 10:21:54 +0000 |
| commit | 9b913feb3532c15aad771f914627a7a82743e625 (patch) | |
| tree | 768da5dfa01c8e619683a05f0bf41378c940ad56 | |
| parent | a502c83b5c9878ef30a8f25f945ff0ef7b70f0f6 (diff) | |
Suite révision 10495
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10496 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 2 |
2 files changed, 6 insertions, 1 deletions
@@ -90,6 +90,11 @@ Tactic Language must not be used elsewhere as variables in the same ltac expression (possible source of incompatibility). - New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression. +- "let rec ... in ... " now supports for expressions without explicit + parameters; interpretation is lazy to the contrary of "let ... in ..."; + hence, the "rec" keyword can be used to turn the argument of a + "let ... in ..." into a lazy one. + Tactics diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 6ea0505a0b..567ed7500d 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -35,7 +35,7 @@ type value = | VConstr of constr | VConstr_context of constr | VList of value list - | VRec of value ref + | VRec of (identifier*value) list ref * glob_tactic_expr (* Signature for interpretation: val\_interp and interpretation functions *) and interp_sign = |