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

2 files changed, 34 insertions, 12 deletions

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 *)