Transparent

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

7 files changed, 73 insertions, 60 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 3fb0f67a5..9696557c1 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -344,8 +344,9 @@ let build_id_coercion idf_opt source =
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     ConstantEntry
       { const_entry_body = mkCast (val_f, typ_f);
-	const_entry_type = None } in
-  let sp = declare_constant idf (constr_entry,NeverDischarge,false) in
+	const_entry_type = None;
+        const_entry_opaque = false } in
+  let sp = declare_constant idf (constr_entry,NeverDischarge) in
   ConstRef sp
 
 (* 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f290d684b..5b3e3a59d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -37,26 +37,26 @@ let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
 
 (* 1| Constant definitions *)
 
-let constant_entry_of_com (com,comtypopt) =
+let constant_entry_of_com (com,comtypopt,opacity) =
   let sigma = Evd.empty in
   let env = Global.env() in
   match comtypopt with
       None -> 
 	{ const_entry_body = interp_constr sigma env com;
-	  const_entry_type = None }
+	  const_entry_type = None;
+          const_entry_opaque = opacity }
     | Some comtyp ->
 	let typ = interp_type sigma env comtyp in
 	{ const_entry_body = interp_casted_constr sigma env com typ;
-	  const_entry_type = Some typ }
+	  const_entry_type = Some typ;
+          const_entry_opaque = opacity }
 
 let red_constant_entry ce = function
   | None -> ce
   | Some red ->
       let body = ce.const_entry_body in
-      { const_entry_body = 
-	  reduction_of_redexp red (Global.env()) Evd.empty body; 
-	const_entry_type = 
-	  ce.const_entry_type }
+      { ce with const_entry_body = 
+	  reduction_of_redexp red (Global.env()) Evd.empty body }
 
 let constr_of_constr_entry ce =
   match ce.const_entry_type with
@@ -64,21 +64,21 @@ let constr_of_constr_entry ce =
     | Some t -> mkCast (ce.const_entry_body, t)
 
 let declare_global_definition ident ce n local =
-  let sp = declare_constant ident (ConstantEntry ce,n,false) in
+  let sp = declare_constant ident (ConstantEntry ce,n) in
   if local then
     wARNING [< pr_id ident; 'sTR" is declared as a global definition" >];
   if_verbose message ((string_of_id ident) ^ " is defined");
   ConstRef sp
 
 let definition_body_red red_option ident (local,n) com comtypeopt = 
-  let ce = constant_entry_of_com (com,comtypeopt) in
+  let ce = constant_entry_of_com (com,comtypeopt,false) in
   let ce' = red_constant_entry ce red_option in
   match n with
     | NeverDischarge -> declare_global_definition ident ce' n local
     | 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
+          let sp = declare_variable ident (SectionLocalDef c,n) in
 	  if_verbose message ((string_of_id ident) ^ " is defined");
           if Pfedit.refining () then 
             mSGERRNL [< 'sTR"Warning: Local definition "; pr_id ident; 
@@ -118,7 +118,7 @@ let hypothesis_def_var is_refining ident n c =
     | 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
+          let sp = declare_variable ident (SectionLocalAssum t,n) in
 	  if_verbose message ((string_of_id ident) ^ " is assumed");
           if is_refining then 
             mSGERRNL [< 'sTR"Warning: Variable "; pr_id ident; 
@@ -271,7 +271,7 @@ let build_recursive lnameargsardef =
            let raw_arity = mkProdCit lparams arityc in
            let arity = interp_type sigma env0 raw_arity in
            let _ = declare_variable recname
-	     (SectionLocalAssum arity, NeverDischarge, false) in
+	     (SectionLocalAssum arity, NeverDischarge) in
            (Environ.push_named_assum (recname,arity) env, (arity::arl)))
         (env0,[]) lnameargsardef
     with e ->
@@ -299,8 +299,9 @@ let build_recursive lnameargsardef =
 	         (Array.map (fun id -> Name id) namerec,
                   arrec,
 		  recvec));
-        const_entry_type = None } in
-    let sp = declare_constant fi (ConstantEntry ce, n, false) in
+        const_entry_type = None;
+        const_entry_opaque = false } in
+    let sp = declare_constant fi (ConstantEntry ce, n) in
     (ConstRef sp)
   in 
   (* declare the recursive definitions *)
@@ -312,8 +313,9 @@ let build_recursive lnameargsardef =
     List.fold_left
       (fun subst (f,def) ->
 	 let ce = { const_entry_body = replace_vars subst def;
-		    const_entry_type = None } in
-	 let _ = declare_constant f (ConstantEntry ce,n,false) in
+		    const_entry_type = None;
+                    const_entry_opaque = false } in
+	 let _ = declare_constant f (ConstantEntry ce,n) in
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst (Array.to_list namerec))
@@ -333,7 +335,7 @@ let build_corecursive lnameardef =
            let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
 	   let arity = arj.utj_val in
            let _ = declare_variable recname
-	     (SectionLocalAssum arj.utj_val,NeverDischarge,false) in
+	     (SectionLocalAssum arj.utj_val,NeverDischarge) in
            (Environ.push_named_assum (recname,arity) env, (arity::arl)))
         (env0,[]) lnameardef
     with e -> 
@@ -360,9 +362,10 @@ let build_corecursive lnameardef =
 	  mkCoFix (i, (Array.map (fun id -> Name id) namerec,
                        arrec,
 		       recvec));
-        const_entry_type = None } 
+        const_entry_type = None;
+        const_entry_opaque = false } 
     in
-    let sp = declare_constant fi (ConstantEntry ce,n,false) in
+    let sp = declare_constant fi (ConstantEntry ce,n) in
     (ConstRef sp)
   in 
   let lrefrec = Array.mapi declare namerec in
@@ -372,8 +375,9 @@ let build_corecursive lnameardef =
     List.fold_left
       (fun subst (f,def) ->
 	 let ce = { const_entry_body = replace_vars subst def;
-		    const_entry_type = None } in
-	 let _ = declare_constant f (ConstantEntry ce,n,false) in
+		    const_entry_type = None;
+                    const_entry_opaque = false } in
+	 let _ = declare_constant f (ConstantEntry ce,n) in
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst (Array.to_list namerec))
@@ -406,8 +410,10 @@ let build_scheme lnamedepindsort =
   let n = NeverDischarge in 
   let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in 
   let rec declare decl fi lrecref =
-    let ce = { const_entry_body = decl; const_entry_type = None } in
-    let sp = declare_constant fi (ConstantEntry ce,n,false) in
+    let ce = { const_entry_body = decl;
+               const_entry_type = None;
+               const_entry_opaque = false } in
+    let sp = declare_constant fi (ConstantEntry ce,n) in
     ConstRef sp :: lrecref
   in 
   let lrecref = List.fold_right2 declare listdecl lrecnames [] in
@@ -434,14 +440,18 @@ let apply_tac_not_declare id pft = function
     Pfedit.delete_current_proof ();
     Pfedit.by (tclTHENS cutt [introduction id;exat])
 
-let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
-  strength =
+let save id const strength =
+  let {const_entry_body = pft;
+       const_entry_type = tpo;
+       const_entry_opaque = opacity } = const in
   begin match strength with
     | 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 ()
+	let _ = declare_variable id (SectionLocalDef c,strength)
+        in ()
     | NeverDischarge | DischargeAt _ ->
-        let _ = declare_constant id (ConstantEntry const,strength,opacity)in ()
+        let _ = declare_constant id (ConstantEntry const,strength)
+        in ()
     | NotDeclare -> apply_tac_not_declare id pft tpo
   end;
   if not (strength = NotDeclare) then
@@ -452,7 +462,8 @@ let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
 
 let save_named opacity =
   let id,(const,strength) = Pfedit.cook_proof () in
-  save opacity id const strength
+  let const = { const with const_entry_opaque = opacity } in
+  save id const strength
 
 let check_anonymity id save_ident =
   if atompart_of_id id <> "Unnamed_thm" then
@@ -463,13 +474,15 @@ let check_anonymity id save_ident =
 
 let save_anonymous opacity save_ident =
   let id,(const,strength) = Pfedit.cook_proof () in
+  let const = { const with const_entry_opaque = opacity } in
   check_anonymity id save_ident;
-  save opacity save_ident const strength
+  save save_ident const strength
 
 let save_anonymous_with_strength strength opacity save_ident =
   let id,(const,_) = Pfedit.cook_proof () in
+  let const = { const with const_entry_opaque = opacity } in
   check_anonymity id save_ident;
-  save opacity save_ident const strength
+  save save_ident const strength
 
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 819df64e0..61db7f6c6 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -162,9 +162,9 @@ let inductive_message inds =
 type opacity = bool
 
 type discharge_operation = 
-  | Variable of identifier * section_variable_entry * strength * bool * bool
+  | Variable of identifier * section_variable_entry * strength * bool
   | Parameter of identifier * constr * bool
-  | Constant of section_path * recipe * strength * opacity * bool
+  | Constant of section_path * recipe * strength * bool
   | Inductive of mutual_inductive_entry * bool
   | Class of cl_typ * cl_info_typ
   | Struc of inductive_path * (unit -> struc_typ)
@@ -181,7 +181,7 @@ let process_object oldenv dir sec_sp
   let tag = object_tag lobj in 
   match tag with
     | "VARIABLE" ->
-	let ((id,c,t),cst,stre,sticky) = get_variable_with_constraints sp in
+	let ((id,c,t),cst,stre) = get_variable_with_constraints sp in
 	(* VARIABLE means local (entry Variable/Hypothesis/Local and are *)
 	(* always discharged *)
 (*
@@ -227,7 +227,7 @@ let process_object oldenv dir sec_sp
 	  let r = { d_from = cb;
 		    d_modlist = work_alist;
 		    d_abstract = ids_to_discard } in
-	  let op = Constant (newsp,r,stre,cb.const_opaque,imp) in
+	  let op = Constant (newsp,r,stre,imp) in
           (op :: ops, ids_to_discard, (mods@constl, indl, cstrl))
   
     | "INDUCTIVE" ->
@@ -281,15 +281,15 @@ let process_item oldenv dir sec_sp acc = function
   | (_,_) -> acc
 
 let process_operation = function
-  | Variable (id,expmod_a,stre,sticky,imp) ->
+  | Variable (id,expmod_a,stre,imp) ->
       (* Warning:parentheses needed to get a side-effect from with_implicits *)
-      let _ = with_implicits imp (declare_variable id) (expmod_a,stre,sticky) in
+      let _ = with_implicits imp (declare_variable id) (expmod_a,stre) in
       ()
   | Parameter (spid,typ,imp) ->
       let _ = with_implicits imp (declare_parameter spid) typ in
       constant_message spid
-  | Constant (sp,r,stre,opa,imp) ->
-      with_implicits imp (redeclare_constant sp) (ConstantRecipe r,stre,opa);
+  | Constant (sp,r,stre,imp) ->
+      with_implicits imp (redeclare_constant sp) (ConstantRecipe r,stre);
       constant_message (basename sp)
   | Inductive (mie,imp) ->
       let _ = with_implicits imp declare_mind mie in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 13b2891ec..a146264ed 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -117,9 +117,11 @@ let declare_projections indsp coers fields =
 	   let name = 
 	     try
 	       let proj = instantiate_inductive_section_params proj indsp in
-	       let cie = { const_entry_body = proj; const_entry_type = None} in
+	       let cie = { const_entry_body = proj;
+                           const_entry_type = None;
+                           const_entry_opaque = false } in
 	       let sp =
-		 declare_constant fi (ConstantEntry cie,NeverDischarge,false)
+		 declare_constant fi (ConstantEntry cie,NeverDischarge)
 	       in Some sp
              with Type_errors.TypeError (k,ctx,te) -> begin
                warning_or_error coe (BadTypedProj (fi,k,ctx,te));
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 71740fbd9..3094fbacb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -643,23 +643,26 @@ let _ =
     (fun id_list () ->
        List.iter 
 	 (function 
-	    | VARG_CONSTANT sp -> Global.set_transparent sp
+	    | VARG_QUALID qid ->
+                (match locate_qualid dummy_loc qid with
+                  | ConstRef sp -> Opaque.set_transparent_const sp
+                  | VarRef sp -> Opaque.set_transparent_var (basename sp) 
+                  | _ -> error
+              "cannot set an inductive type or a constructor as transparent")
 	    |   _  -> bad_vernac_args "TRANSPARENT")
 	 id_list)
 
-let warning_opaque s =
-  if_verbose warning
-      ("This command turns the constants which depend on the definition/proof
-of "^s^" un-re-checkable until the next \"Transparent "^s^"\" command.")
-
 let _ =
   add "OPAQUE"
     (fun id_list () ->
        List.iter
 	 (function 
-	    | VARG_CONSTANT sp ->
-		warning_opaque (Global.string_of_global (ConstRef sp));
-		Global.set_opaque sp
+	    | VARG_QUALID qid ->
+                (match locate_qualid dummy_loc qid with
+                  | ConstRef sp -> Opaque.set_opaque_const sp
+                  | VarRef sp -> Opaque.set_opaque_var (basename sp) 
+                  | _ -> error
+             "cannot set an inductive type or a constructor as opaque")
 	    |   _  -> bad_vernac_args "OPAQUE")
 	 id_list)
 
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 3d170e6be..0b32cd141 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -32,7 +32,6 @@ type vernac_arg =
   | VARG_NUMBERLIST of int list
   | VARG_IDENTIFIER of identifier
   | VARG_QUALID of Nametab.qualid
-  | VARG_CONSTANT of constant_path
   | VCALL of string * vernac_arg list
   | VARG_CONSTR of Coqast.t
   | VARG_CONSTRLIST of Coqast.t list
@@ -85,12 +84,6 @@ let rec cvt_varg ast =
 
     | Nvar(_,id) -> VARG_IDENTIFIER id
     | Node(loc,"QUALIDARG",p) -> VARG_QUALID (Astterm.interp_qualid p)
-    | Node(loc,"QUALIDCONSTARG",p) ->
-	let q = Astterm.interp_qualid p in
-	let sp =
-	  try Nametab.locate_constant q
-	  with Not_found -> Nametab.error_global_constant_not_found_loc loc q
-	in VARG_CONSTANT sp
     | Str(_,s) -> VARG_STRING s
     | Id(_,s) -> VARG_STRING s
     | Num(_,n) -> VARG_NUMBER n
@@ -112,7 +105,9 @@ let rec cvt_varg ast =
     | Node(_,"ASTLIST",al) -> VARG_ASTLIST al
     | Node(_,"TACTIC_ARG",[targ]) ->
       let (evc,env)= Command.get_current_context () in
-      VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None,get_debug ()) targ)
+      let ist = { evc=evc; env=env; lfun=[]; lmatch=[];
+                  goalopt=None; debug=get_debug ()} in
+      VARG_TACTIC_ARG (interp_tacarg ist targ)
     | Node(_,"VERNACDYN",[Dynamic (_,d)]) -> VARG_DYN d
     | _ -> anomaly_loc (Ast.loc ast, "Vernacinterp.cvt_varg",
                         [< 'sTR "Unrecognizable ast node of vernac arg:";
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index ed068d167..2aa45f322 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -28,7 +28,6 @@ type vernac_arg =
   | VARG_NUMBERLIST of int list
   | VARG_IDENTIFIER of identifier
   | VARG_QUALID of Nametab.qualid
-  | VARG_CONSTANT of constant_path
   | VCALL of string * vernac_arg list
   | VARG_CONSTR of Coqast.t
   | VARG_CONSTRLIST of Coqast.t list