diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-01 10:21:54 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-01 10:21:54 +0000 |
| commit | 9b913feb3532c15aad771f914627a7a82743e625 (patch) | |
| tree | 768da5dfa01c8e619683a05f0bf41378c940ad56 /tactics | |
| 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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 6ea0505a0..567ed7500 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 = |