From a3645985be17e9fa8a8a5c4221aea40e189682c2 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 14 Sep 2009 16:57:14 +0000
Subject: Backtrack on the forced discharge of type class variables introduced
 by Context. Now Context has exactly the same semantics as Variables.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12329 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'library/declare.ml')

diff --git a/library/declare.ml b/library/declare.ml
index 0cd1250c7f..44536ce5b3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -46,7 +46,7 @@ let add_cache_hook f = cache_hook := f
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep *)
+  | SectionLocalAssum of types * bool (* Implicit status *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
@@ -57,17 +57,16 @@ let cache_variable ((sp,_),o) =
   (* Constr raisonne sur les noms courts *)
   if variable_exists id then
     errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
-  let impl,opaq,cst,keep = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum (ty, impl, keep) ->
+  let impl,opaq,cst = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum (ty, impl) ->
         let cst = Global.push_named_assum (id,ty) in
 	let impl = if impl then Lib.Implicit else Lib.Explicit in
-	let keep = if keep <> [] then Some (ty, keep) else None in
-	impl, true, cst, keep
+	impl, true, cst
     | SectionLocalDef (c,t,opaq) -> 
         let cst = Global.push_named_def (id,c,t) in
-        Lib.Explicit, opaq, cst, None in
+        Lib.Explicit, opaq, cst in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  add_section_variable id impl keep;
+  add_section_variable id impl;
   Dischargedhypsmap.set_discharged_hyps sp [];
   add_variable_data id (p,opaq,cst,mk)
 
-- 
cgit v1.2.3