caractere opaque des constantes repris en compte

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

9 files changed, 44 insertions, 26 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 4c68617c24..f86edc915d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -114,7 +114,9 @@ type constant_declaration_type =
   | ConstantEntry  of constant_entry
   | ConstantRecipe of Cooking.recipe
 
-type constant_declaration = constant_declaration_type * strength
+type opacity = bool
+
+type constant_declaration = constant_declaration_type * strength * opacity
 
 let csttab = ref (Spmap.empty : strength Spmap.t)
 
@@ -124,7 +126,7 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.init_function = (fun () -> csttab := Spmap.empty);
 	    Summary.survive_section = false }
 
-let cache_constant (sp,(cdt,stre)) =
+let cache_constant (sp,(cdt,stre,op)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_constant"
       [< pr_id (basename sp); 'sTR " already exists" >] ;
@@ -133,9 +135,10 @@ let cache_constant (sp,(cdt,stre)) =
     | ConstantRecipe r -> Global.add_discharged_constant sp r
   end;
   Nametab.push sp (ConstRef sp);
+  if op then Global.set_opaque sp;
   csttab := Spmap.add sp stre !csttab
 
-let load_constant (sp,(ce,stre)) =
+let load_constant (sp,(ce,stre,op)) =
   csttab := Spmap.add sp stre !csttab
 
 let open_constant (sp,_) = ()
@@ -437,7 +440,7 @@ let declare_eliminations sp i =
   let declare na c =
     declare_constant (id_of_string na)
       (ConstantEntry { const_entry_body = c; const_entry_type = None }, 
-       NeverDischarge);
+       NeverDischarge,false);
     if Options.is_verbose() then pPNL [< 'sTR na; 'sTR " is defined" >]
   in
   let env = Global.env () in
diff --git a/library/declare.mli b/library/declare.mli
index 78f19e68f8..38a14c0107 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -34,7 +34,9 @@ type constant_declaration_type =
   | ConstantEntry  of constant_entry
   | ConstantRecipe of Cooking.recipe
 
-type constant_declaration = constant_declaration_type * strength
+type opacity = bool
+
+type constant_declaration = constant_declaration_type * strength * opacity
 
 val declare_constant : identifier -> constant_declaration -> unit
 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 9290fd5a1c..238a1a0c51 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,7 +232,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof = inversion_scheme env sigma t sort dep inv_op in
   declare_constant name
     (ConstantEntry { const_entry_body = invProof; const_entry_type = None }, 
-     NeverDischarge)
+     NeverDischarge,false)
 
 (* open Pfedit *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0e26d170e4..b45ba9d795 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1679,7 +1679,7 @@ let abstract_subproof name tac gls =
       with e when catchable_exception e -> 
 	(delete_current_proof(); raise e)
     in   (* Faudrait un peu fonctionnaliser cela *)
-    Declare.declare_constant na (ConstantEntry const,strength);
+    Declare.declare_constant na (ConstantEntry const,strength,true);
     let newenv = Global.env() in
     Declare.construct_reference newenv CCI na
   in
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 29a8b0a66a..54845ea07d 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -65,7 +65,7 @@ Save.
      | (or_intror neqxy) => (False_ind ? (neqxy u))
      end.
 
-  Remark nu_constant : (y:A)(u,v:x==y) (nu u)==(nu v).
+  Local nu_constant : (y:A)(u,v:x==y) (nu u)==(nu v).
 Intros.
 Unfold nu.
 Elim (eq_dec x y) using or_indd; Intros.
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 7b803fb4d6..e133c87ea7 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -262,7 +262,7 @@ let build_id_coercion idf_opt ids =
   in
   let constr_entry = 
     { const_entry_body = val_f; const_entry_type = None } in
-  declare_constant idf (ConstantEntry constr_entry,NeverDischarge);
+  declare_constant idf (ConstantEntry constr_entry,NeverDischarge,false);
   idf
 
 let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index eef22b8a25..caa6d05d67 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -49,6 +49,11 @@ let red_constant_entry ce = function
 	const_entry_type = 
 	  ce.const_entry_type }
 
+let constr_of_constr_entry ce =
+  match ce.const_entry_type with
+    | None -> ce.const_entry_body 
+    | Some t -> mkCast (ce.const_entry_body, t)
+
 let definition_body_red red_option ident (local,n) com comtypeopt = 
   let warning () = 
     mSGERRNL [< 'sTR"Warning: "; pr_id ident; 
@@ -57,21 +62,19 @@ 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_constant ident (ConstantEntry ce',n);
+	declare_constant ident (ConstantEntry ce',n,false);
 	if local then warning ();
 	if is_verbose() then message ((string_of_id ident) ^ " is defined")
     | DischargeAt disch_sp ->
         if Lib.is_section_p disch_sp then begin
-	  let c = match ce.const_entry_type with
-	    | None -> ce.const_entry_body 
-	    | Some t -> mkCast (ce.const_entry_body, t) in
+	  let c = constr_of_constr_entry ce in
           declare_variable ident (SectionLocalDef c,n,false);
 	  if is_verbose() then message ((string_of_id ident) ^ " is defined");
           if Pfedit.refining () then 
             mSGERRNL [< 'sTR"Warning: Variable "; pr_id ident; 
                         'sTR" is not visible from current goals" >]
         end else begin
-	  declare_constant ident (ConstantEntry ce',n);
+	  declare_constant ident (ConstantEntry ce',n,false);
 	  warning ();
 	  if is_verbose() then message ((string_of_id ident) ^ " is defined")
 	end
@@ -266,7 +269,7 @@ let build_recursive lnameargsardef =
 			recvec));
 	      const_entry_type = None } 
 	  in
-	  declare_constant fi (ConstantEntry ce, n);
+	  declare_constant fi (ConstantEntry ce, n, false);
           declare (i+1) lf
       | _ -> () 
     in 
@@ -281,7 +284,7 @@ let build_recursive lnameargsardef =
       (fun subst (f,def) ->
 	 let ce = { const_entry_body = replace_vars subst def;
 		    const_entry_type = None } in
-	 declare_constant f (ConstantEntry ce,n);
+	 declare_constant f (ConstantEntry ce,n,false);
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst lnamerec)
@@ -335,7 +338,7 @@ let build_corecursive lnameardef =
 			     recvec));
 	      const_entry_type = None } 
 	  in
-          declare_constant fi (ConstantEntry ce,n);
+          declare_constant fi (ConstantEntry ce,n,false);
           declare (i+1) lf
       | _        -> () 
     in 
@@ -348,7 +351,7 @@ let build_corecursive lnameardef =
       (fun subst (f,def) ->
 	 let ce = { const_entry_body = replace_vars subst def;
 		    const_entry_type = None } in
-	 declare_constant f (ConstantEntry ce,n);
+	 declare_constant f (ConstantEntry ce,n,false);
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst lnamerec)
@@ -381,7 +384,7 @@ let build_scheme lnamedepindsort =
   let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in 
   let rec declare decl fi =
     let ce = { const_entry_body = decl; const_entry_type = None } 
-    in declare_constant fi (ConstantEntry ce,n)
+    in declare_constant fi (ConstantEntry ce,n,false)
   in 
   List.iter2 declare listdecl lrecnames; 
   if is_verbose() then pPNL(recursive_message lrecnames)
@@ -399,7 +402,13 @@ let start_proof_com sopt stre com =
 
 let save_named opacity =
   let id,(const,strength) = Pfedit.cook_proof () in
-  declare_constant id (ConstantEntry const,strength);
+  begin match strength with
+    | DischargeAt disch_sp when Lib.is_section_p disch_sp ->
+	let c = constr_of_constr_entry const in
+	declare_variable id (SectionLocalDef c,strength,opacity)
+    | _ ->
+	declare_constant id (ConstantEntry const,strength,opacity)
+  end;
   Pfedit.delete_current_proof ();
   if Options.is_verbose() then message ((string_of_id id) ^ " is defined")
 
@@ -407,7 +416,8 @@ let save_anonymous opacity save_ident strength =
   let id,(const,_) = Pfedit.cook_proof () in
   if atompart_of_id id <> "Unnamed_thm" then
     message("Overriding name "^(string_of_id id)^" and using "^save_ident);
-  declare_constant (id_of_string save_ident) (ConstantEntry const,strength);
+  declare_constant 
+    (id_of_string save_ident) (ConstantEntry const,strength,opacity);
   Pfedit.delete_current_proof ();
   if Options.is_verbose() then message (save_ident ^ " is defined")
 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index bfdb60c902..25b1383c35 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -126,10 +126,12 @@ let inductive_message inds =
 
 (* Discharge operations for the various objects of the environment. *)
 
+type opacity = bool
+
 type discharge_operation = 
   | Variable of identifier * section_variable_entry * strength * bool * bool
   | Parameter of identifier * constr * bool
-  | Constant of identifier * recipe * strength * bool
+  | Constant of identifier * recipe * strength * opacity * bool
   | Inductive of mutual_inductive_entry * bool
   | Class of cl_typ * cl_info_typ
   | Struc of inductive_path * struc_typ
@@ -177,7 +179,7 @@ let process_object oldenv dir sec_sp
 	  let r = { d_from = sp;
 		    d_modlist = work_alist;
 		    d_abstract = ids_to_discard } in
-	  let op = Constant (spid,r,stre,imp) in
+	  let op = Constant (spid,r,stre,cb.const_opaque,imp) in
           (op :: ops, ids_to_discard, (mods@constl, indl, cstrl))
   
     | "INDUCTIVE" ->
@@ -236,8 +238,8 @@ let process_operation = function
   | Parameter (spid,typ,imp) ->
       with_implicits imp (declare_parameter spid) typ;
       constant_message spid
-  | Constant (spid,r,stre,imp) ->
-      with_implicits imp (declare_constant spid) (ConstantRecipe r,stre);
+  | Constant (spid,r,stre,opa,imp) ->
+      with_implicits imp (declare_constant spid) (ConstantRecipe r,stre,opa);
       constant_message spid
   | Inductive (mie,imp) ->
       let _ = with_implicits imp declare_mind mie in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 9fe9142c13..f08c7dcfd9 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -141,7 +141,8 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
 	       let cie =
 		 { const_entry_body = proj;
 		   const_entry_type = None } in
-	       (declare_constant fi (ConstantEntry cie,NeverDischarge); true)
+	       (declare_constant fi (ConstantEntry cie,NeverDischarge,false); 
+		true)
              with Type_errors.TypeError (k,ctx,te) ->
                ((warning_or_error coe 
                    [<'sTR (string_of_id fi);