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

4 files changed, 15 insertions, 21 deletions

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)
 
diff --git a/library/declare.mli b/library/declare.mli
index d5933ffb0d..94457a9f84 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -34,7 +34,7 @@ open Nametab
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
-  | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep list *)
+  | SectionLocalAssum of types * bool (* Implicit status *)
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
diff --git a/library/lib.ml b/library/lib.ml
index 1a3a07e013..197e4c3f1e 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -438,24 +438,20 @@ type variable_context = variable_info list
 type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
 
 let sectab =
-  ref ([] : ((Names.identifier * binding_kind * (Term.types * Names.identifier list) option) list * Cooking.work_list * abstr_list) list)
+  ref ([] : ((Names.identifier * binding_kind) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
 
-let add_section_variable id impl keep =
+let add_section_variable id impl =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-	sectab := ((id,impl,keep)::vars,repl,abs)::sl
+	sectab := ((id,impl)::vars,repl,abs)::sl
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: aux (idl,hyps)
-    | ((id,impl,Some (ty,keep))::idl,hyps) -> 
-	if List.exists (fun (id,_,_) -> List.mem id keep) ohyps then
-	  (id,impl,None,ty) :: aux (idl,hyps)
-	else aux (idl,hyps)
+    | ((id,impl)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: aux (idl,hyps)
     | (id::idl,hyps) -> aux (idl,hyps)
     | [], _ -> []
   in aux (secs,ohyps)
@@ -495,13 +491,13 @@ let section_segment_of_constant con =
 let section_segment_of_mutual_inductive kn =
   Names.KNmap.find kn (snd (pi3 (List.hd !sectab)))
 
-let rec list_mem_assoc_in_triple x = function
+let rec list_mem_assoc x = function
   | [] -> raise Not_found
-  | (a,_,_)::l -> compare a x = 0 or list_mem_assoc_in_triple x l
+  | (a,_)::l -> compare a x = 0 or list_mem_assoc x l
 
 let section_instance = function
   | VarRef id ->
-      if list_mem_assoc_in_triple id (pi1 (List.hd !sectab)) then [||]
+      if list_mem_assoc id (pi1 (List.hd !sectab)) then [||]
       else raise Not_found
   | ConstRef con ->
       Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
diff --git a/library/lib.mli b/library/lib.mli
index 1207511f09..f4d4900c32 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -180,8 +180,7 @@ val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_cont
 val section_instance : Libnames.global_reference -> Names.identifier array
 val is_in_section : Libnames.global_reference -> bool
 
-val add_section_variable : Names.identifier -> binding_kind -> 
-  (Term.types * Names.identifier list) option -> unit
+val add_section_variable : Names.identifier -> binding_kind -> unit
 
 val add_section_constant : Names.constant -> Sign.named_context -> unit
 val add_section_kn : Names.kernel_name -> Sign.named_context -> unit