diff options
| author | msozeau | 2008-05-11 22:04:26 +0000 |
|---|---|---|
| committer | msozeau | 2008-05-11 22:04:26 +0000 |
| commit | 30443ddaba7a0cc996216b3d692b97e0b05907fe (patch) | |
| tree | 1a1bdadcdf69582262bd6bddc21e9e03215d2871 /kernel | |
| parent | b6c6e36afa8da16a62bf16191baa2531894c54fc (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')
| -rw-r--r-- | kernel/names.ml | 1 | ||||
| -rw-r--r-- | kernel/names.mli | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index d1c6ee8a44..975390cb9e 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -320,6 +320,7 @@ type transparent_state = Idpred.t * Cpred.t let empty_transparent_state = (Idpred.empty, Cpred.empty) let full_transparent_state = (Idpred.full, Cpred.full) let var_full_transparent_state = (Idpred.full, Cpred.empty) +let cst_full_transparent_state = (Idpred.empty, Cpred.full) type 'a tableKey = | ConstKey of constant diff --git a/kernel/names.mli b/kernel/names.mli index 340f6e812f..b19f93e2d9 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -172,6 +172,7 @@ type transparent_state = Idpred.t * Cpred.t val empty_transparent_state : transparent_state val full_transparent_state : transparent_state val var_full_transparent_state : transparent_state +val cst_full_transparent_state : transparent_state type inv_rel_key = int (* index in the [rel_context] part of environment starting by the end, {\em inverse} |