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, 9 insertions, 20 deletions

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