- déplacement (encore une fois !) des variables existentielles : elles sont

   toujours dans le noyau (en ce sens que Reduction et Typeops les
   connaissent) mais dans un argument supplémentaire A COTE de l'environnement
   (de type unsafe_env)
 - Indtypes et Typing n'utilisent strictement que Evd.empty


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@106 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 0 deletions

diff --git a/library/declare.ml b/library/declare.ml
index cb5ec1b40..64445cf5e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -12,6 +12,10 @@ open Libobject
 open Lib
 open Impargs
 
+type strength = 
+  | DischargeAt of section_path 
+  | NeverDischarge
+
 (* Variables. *)
 
 let cache_variable (_,obj) =