- 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

1 files changed, 1 insertions, 0 deletions

diff --git a/kernel/names.mli b/kernel/names.mli
index 340f6e812..b19f93e2d 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}