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 /kernel/make-opcodes | |
| 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 'kernel/make-opcodes')
0 files changed, 0 insertions, 0 deletions