Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le «load» des Remark/Fact

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

3 files changed, 7 insertions, 7 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 667e127061..3fb0f67a5b 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -36,7 +36,7 @@ let stre_gt = function
   | (NotDeclare,_) -> false
   | (_,NeverDischarge) -> true
   | (_,NotDeclare) -> true
-  | (DischargeAt sp1,DischargeAt sp2) ->
+  | (DischargeAt (sp1,_),DischargeAt (sp2,_)) ->
       is_dirpath_prefix_of sp1 sp2
 	(* was sp_gt but don't understand why - HH *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f53f26b8d4..f290d684b3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -75,7 +75,7 @@ let definition_body_red red_option ident (local,n) com comtypeopt =
   let ce' = red_constant_entry ce red_option in
   match n with
     | NeverDischarge -> declare_global_definition ident ce' n local
-    | DischargeAt disch_sp ->
+    | DischargeAt (disch_sp,_) ->
         if Lib.is_section_p disch_sp then begin
 	  let c = constr_of_constr_entry ce' in
           let sp = declare_variable ident (SectionLocalDef c,n,false) in
@@ -115,7 +115,7 @@ let declare_global_assumption ident c =
 let hypothesis_def_var is_refining ident n c =
   match n with
     | NeverDischarge -> declare_global_assumption ident c
-    | DischargeAt disch_sp ->
+    | DischargeAt (disch_sp,_) ->
         if Lib.is_section_p disch_sp then begin
 	  let t = interp_type Evd.empty (Global.env()) c in
           let sp = declare_variable ident (SectionLocalAssum t,n,false) in
@@ -437,7 +437,7 @@ let apply_tac_not_declare id pft = function
 let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
   strength =
   begin match strength with
-    | DischargeAt disch_sp when Lib.is_section_p disch_sp && not opacity ->
+    | DischargeAt (disch_sp,_) when Lib.is_section_p disch_sp && not opacity ->
 	let c = constr_of_constr_entry const in
 	let _ = declare_variable id (SectionLocalDef c,strength,opacity) in ()
     | NeverDischarge | DischargeAt _ ->
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 730817bf34..819df64e03 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -218,7 +218,7 @@ let process_object oldenv dir sec_sp
 	  let cb = Environ.lookup_constant sp oldenv in
 	  let imp = is_implicit_constant sp in
 	  let newsp = match stre with
-	    | DischargeAt d when not (is_dirpath_prefix_of d dir) -> sp
+	    | DischargeAt (d,_) when not (is_dirpath_prefix_of d dir) -> sp
 	    | _ -> recalc_sp dir sp in
 	  let mods = 
 	    let modl = build_abstract_list cb.const_hyps ids_to_discard in
@@ -241,7 +241,7 @@ let process_object oldenv dir sec_sp
 
     | "CLASS" -> 
 	let ((cl,clinfo) as x) = outClass lobj in
-	if clinfo.cl_strength = (DischargeAt sec_sp) then 
+	if (match clinfo.cl_strength with DischargeAt (sp,_) -> sp = sec_sp | _ -> false) then 
 	  (ops,ids_to_discard,work_alist)
 	else
 	  let (y1,y2) = process_class sec_sp ids_to_discard x in
@@ -249,7 +249,7 @@ let process_object oldenv dir sec_sp
 	  
     | "COERCION" -> 
 	let (((_,coeinfo),_,_)as x) = outCoercion lobj in
-        if coercion_strength coeinfo = (DischargeAt sec_sp) then 
+	if (match coercion_strength coeinfo with DischargeAt (sp,_) -> sp = sec_sp | _ -> false) then 
 	  (ops,ids_to_discard,work_alist)
         else
 	  let y = process_coercion sec_sp ids_to_discard x in