aboutsummaryrefslogtreecommitdiff
path: root/kernel/indtypes.ml
diff options
context:
space:
mode:
authormsozeau2008-05-11 22:04:26 +0000
committermsozeau2008-05-11 22:04:26 +0000
commit30443ddaba7a0cc996216b3d692b97e0b05907fe (patch)
tree1a1bdadcdf69582262bd6bddc21e9e03215d2871 /kernel/indtypes.ml
parentb6c6e36afa8da16a62bf16191baa2531894c54fc (diff)
- Cleanup parsing of binders, reducing to a single production for all
binders. - Change syntax of type class instances to better match the usual syntax of lemmas/definitions with name first, then arguments ":" instance. Update theories/Classes accordingly. - Correct globalization of tactic references when doing Ltac :=/::=, update documentation. - Remove the not so useful "(x &)" and "{{x}}" syntaxes from Program.Utils, and subset_scope as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions