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

9 files changed, 25 insertions, 42 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 0cd1250c7..44536ce5b 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 d5933ffb0..94457a9f8 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 1a3a07e01..197e4c3f1 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 1207511f0..f4d4900c3 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
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 8b1d20e6d..b5e288013 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -101,7 +101,7 @@ let declare_assumption env isevars idl is_coe k bl c nl =
       Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None 
     in
     let c = solve_tccs_in_type env id isevars evm c typ in
-      List.iter (Command.declare_one_assumption is_coe k c imps false [] nl) idl
+      List.iter (Command.declare_one_assumption is_coe k c imps false nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 91bf5cd21..2eeb8a7de 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -275,14 +275,6 @@ let context ?(hook=fun _ -> ()) l =
   let ctx = try named_of_rel_context fullctx with _ -> 
     error "Anonymous variables not allowed in contexts."
   in
-  let env = push_named_context ctx env in
-  let keeps = 
-    List.fold_left (fun acc (id,_,t) ->
-      match class_of_constr t with
-      | None -> acc
-      | Some _ -> List.map pi1 (keep_hyps env (Idset.singleton id)) :: acc)
-      [] ctx
-  in
     List.iter (function (id,_,t) -> 
       if Lib.is_modtype () then 
 	let cst = Declare.declare_internal_constant id
@@ -296,12 +288,9 @@ let context ?(hook=fun _ -> ()) l =
       else (
 	let impl = List.exists (fun (x,_) -> 
 	  match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls 
-	and keep = 
-	  let l = list_filter_map (fun ids -> if List.mem id ids then Some ids else None) keeps in
-	    List.concat l
 	in
 	  Command.declare_one_assumption false (Local (* global *), Definitional) t
-	    [] impl (* implicit *) keep (* always kept *) false (* inline *) (dummy_loc, id);
+	    [] impl (* implicit *) false (* inline *) (dummy_loc, id);
 	  match class_of_constr t with
 	  | None -> ()
 	  | Some tc -> hook (VarRef id)))
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 80de34458..1da86712d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -169,12 +169,12 @@ let syntax_definition ident (vars,c) local onlyparse =
 let assumption_message id =
   if_verbose message ((string_of_id id) ^ " is assumed")
 
-let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) =
+let declare_one_assumption is_coe (local,kind) c imps impl nl (_,ident) =
   let r = match local with
     | Local when Lib.sections_are_opened () ->
         let _ = 
           declare_variable ident 
-            (Lib.cwd(), SectionLocalAssum (c,impl,keep), IsAssumption kind) in
+            (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in
         assumption_message ident;
         if is_verbose () & Pfedit.refining () then 
           msgerrnl (str"Warning: Variable " ++ pr_id ident ++ 
@@ -196,13 +196,13 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) =
 let declare_assumption_hook = ref ignore
 let set_declare_assumption_hook = (:=) declare_assumption_hook
 
-let declare_assumption idl is_coe k bl c impl keep nl =
+let declare_assumption idl is_coe k bl c impl nl =
   if not (Pfedit.refining ()) then 
     let c = generalize_constr_expr c bl in
     let env = Global.env () in
     let c', imps = interp_type_evars_impls env c in
       !declare_assumption_hook c';
-      List.iter (declare_one_assumption is_coe k c' imps impl keep nl) idl
+      List.iter (declare_one_assumption is_coe k c' imps impl nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
@@ -1106,7 +1106,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) =
       | Local ->
           let impl=false in (* copy values from Vernacentries *)
           let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum (t_i,impl,[]) in
+          let c = SectionLocalAssum (t_i,impl) in
 	  let _ = declare_variable id (Lib.cwd(),c,k) in
           (Local,VarRef id,imps)
       | Global ->
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d5283a6db..d648fc10e 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -45,13 +45,13 @@ val syntax_definition : identifier -> identifier list * constr_expr ->
 
 val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
   Impargs.manual_explicitation list ->
-  bool (* implicit *) -> identifier list (* keep *) -> bool (* inline *) -> Names.variable located  -> unit
+  bool (* implicit *) -> bool (* inline *) -> Names.variable located  -> unit
   
 val set_declare_assumption_hook : (types -> unit) -> unit
 
 val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> 
-  bool -> identifier list -> bool -> unit
+  bool -> bool -> unit
 
 val open_temp_scopes : Topconstr.scope_name option -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 887d5a616..be7c29bab 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -373,7 +373,7 @@ let vernac_assumption kind l nl=
 	List.iter (fun lid -> 
 	  if global then Dumpglob.dump_definition lid false "ax" 
 	  else Dumpglob.dump_definition lid true "var") idl;
-      declare_assumption idl is_coe kind [] c false [] nl) l
+      declare_assumption idl is_coe kind [] c false nl) l
 	  
 let vernac_record k finite infer struc binders sort nameopt cfs =
   let const = match nameopt with