From 30443ddaba7a0cc996216b3d692b97e0b05907fe Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 11 May 2008 22:04:26 +0000
Subject: - 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
---
 kernel/names.ml  | 1 +
 kernel/names.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'kernel')

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} 
-- 
cgit v1.2.3