diff options
| author | msozeau | 2006-03-22 18:55:41 +0000 |
|---|---|---|
| committer | msozeau | 2006-03-22 18:55:41 +0000 |
| commit | 64da3b4eac7d8d35bfd983e9f73bd1ff1bdcc216 (patch) | |
| tree | 4b80a051d5013124fec64641bd0157551dfe239f /pretyping/pretyping.mli | |
| parent | 10961655cb9c09da20cfe2ecc68def3d3b7d1bb5 (diff) | |
Subtac fixes, single fixpoint definitions are working again. Added a toggle on the pretyping
module to allow or disallow binding of syntaxically inexistant variables (i.e., under an if when applied to an inductive where
constructors have arguments). Does not change current behavior.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8655 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index f93e461298..ac8e6fec78 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -27,7 +27,10 @@ module type S = sig module Cases : Cases.S - + + (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *) + val allow_anonymous_refs : bool ref + (* Generic call to the interpreter from rawconstr to open_constr, leaving unresolved holes as evars and returning the typing contexts of these evars. Work as [understand_gen] for the rest. *) |