Suppression automatique du corps des définitions locales opaques dans

les contextes de preuves


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

4 files changed, 39 insertions, 15 deletions

diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index a2baceade2..14d0f94ac0 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -871,7 +871,7 @@ let print_object lobj id (sp,kn) dn fv env =
           let (_,(_,varentry,_)) = Declare.out_variable lobj in
            begin
             match varentry with
-               Declare.SectionLocalDef (body,optt) ->
+               Declare.SectionLocalDef (body,optt,_) ->
                  let typ = match optt with
 		   | None -> Retyping.get_type_of env Evd.empty body 
 		   | Some t -> t in
diff --git a/library/declare.ml b/library/declare.ml
index 31af6dbbb8..91b58d092f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -75,12 +75,14 @@ let strength_min (stre1,stre2) =
 (* Section variables. *)
 
 type section_variable_entry =
-  | SectionLocalDef of constr * types option
+  | SectionLocalDef of constr * types option * bool (* opacity *)
   | SectionLocalAssum of types
 
 type variable_declaration = dir_path * section_variable_entry * strength
 
-type checked_section_variable = constr option * types * Univ.constraints
+type checked_section_variable =
+  | CheckedSectionLocalDef of constr * types * Univ.constraints * bool
+  | CheckedSectionLocalAssum of types * Univ.constraints
 
 type checked_variable_declaration =
     dir_path * checked_section_variable * strength
@@ -97,11 +99,15 @@ let cache_variable ((sp,_),(id,(p,d,strength))) =
   (* Constr raisonne sur les noms courts *)
   if Idmap.mem id !vartab then
     errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
-  let cst = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum ty -> Global.push_named_assum (id,ty)
-    | SectionLocalDef (c,t) -> Global.push_named_def (id,c,t) in
-  let (_,bd,ty) = Global.lookup_named id in
-  let vd = (bd,ty,cst) in
+  let vd = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum ty ->
+        let cst = Global.push_named_assum (id,ty) in
+        let (_,bd,ty) = Global.lookup_named id in
+        CheckedSectionLocalAssum (ty,cst)
+    | SectionLocalDef (c,t,opaq) -> 
+        let cst = Global.push_named_def (id,c,t) in
+        let (_,bd,ty) = Global.lookup_named id in
+        CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   vartab := Idmap.add id (p,vd,strength) !vartab
 
@@ -294,12 +300,17 @@ let is_constant sp =
 let constant_strength sp = Spmap.find sp !csttab
 
 let get_variable id = 
-  let (p,(c,ty,cst),str) = Idmap.find id !vartab in
-  ((id,c,ty),str)
+  let (p,x,str) = Idmap.find id !vartab in
+  let d = match x with
+    | CheckedSectionLocalDef (c,ty,cst,opaq) -> (id,Some c,ty)
+    | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty) in
+  (d,str)
 
 let get_variable_with_constraints id = 
-  let (p,(c,ty,cst),str) = Idmap.find id !vartab in
-  ((id,c,ty),cst,str)
+  let (p,x,str) = Idmap.find id !vartab in
+  match x with
+    | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst,str)
+    | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst,str)
 
 let variable_strength id =
   let (_,_,str) = Idmap.find id !vartab in str
@@ -307,6 +318,16 @@ let variable_strength id =
 let find_section_variable id =
   let (p,_,_) = Idmap.find id !vartab in Libnames.make_path p id
 
+let variable_opacity id =
+  let (_,x,_) = Idmap.find id !vartab in
+  match x with
+    | CheckedSectionLocalDef (c,ty,cst,opaq) -> opaq
+    | CheckedSectionLocalAssum (ty,cst) -> false (* any.. *)
+
+let clear_proofs sign =
+  List.map
+    (fun (id,c,t as d) -> if variable_opacity id then (id,None,t) else d) sign
+
 (* Global references. *)
 
 let first f v =
diff --git a/library/declare.mli b/library/declare.mli
index 273a2b3440..c9d7cc5740 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -31,7 +31,7 @@ open Nametab
 open Nametab
 
 type section_variable_entry =
-  | SectionLocalDef of constr * types option
+  | SectionLocalDef of constr * types option * bool (* opacity *)
   | SectionLocalAssum of types
 
 type variable_declaration = dir_path * section_variable_entry * strength
@@ -76,6 +76,7 @@ val get_variable_with_constraints :
 val variable_strength : variable -> strength
 val find_section_variable : variable -> section_path
 val last_section_hyps : dir_path -> identifier list
+val clear_proofs : named_context -> named_context
 
 (*s Global references *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c9becbd3ac..01b883998f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -107,7 +107,8 @@ let declare_definition ident (local,n) bl red_option c typopt =
     | NeverDischarge -> declare_global_definition ident ce' n local
     | DischargeAt (disch_sp,_) ->
         if Lib.is_section_p disch_sp then begin
-	  let c = SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type) in
+	  let c =
+            SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in
           let _ = declare_variable ident (Lib.cwd(), c, n) in
 	  if_verbose message ((string_of_id ident) ^ " is defined");
           if Pfedit.refining () then 
@@ -472,6 +473,7 @@ let build_scheme lnamedepindsort =
 let start_proof_com sopt (local,stre) com hook =
   let env = Global.env () in
   let sign = Global.named_context () in
+  let sign = clear_proofs sign in
   let id = match sopt with
     | Some id ->
         (* We check existence here: it's a bit late at Qed time *)
@@ -500,7 +502,7 @@ let save id const (local,strength) hook =
        const_entry_opaque = opacity } = const in
   begin match strength with
     | DischargeAt (disch_sp,_) when Lib.is_section_p disch_sp && local ->
-	let c = SectionLocalDef (pft, tpo) in
+	let c = SectionLocalDef (pft, tpo, opacity) in
 	let _ = declare_variable id (Lib.cwd(), c, strength) in
 	hook strength (VarRef id)
     | NeverDischarge | DischargeAt _ ->