Transparent

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

6 files changed, 9 insertions, 11 deletions

diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 5cdd5eacd..9e5f95439 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -58,10 +58,7 @@ Proof.
   Elim (eq_nat_dec n n0);Intro y.
   Left; Rewrite y; Auto.
   Right;Red;Intro;Inversion H;Auto. 
-Save.
-
-Transparent Peano_dec.eq_nat_dec.
-Transparent eqExprA_O.
+Defined.
 
 Definition eq_nat_dec := Eval Compute in Peano_dec.eq_nat_dec.
 Definition eqExprA := Eval Compute in eqExprA_O.
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 926ca7951..61bd3353f 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -109,8 +109,10 @@ let _ =
 let field g =
   let evc = project g
   and env = pf_env g in
-  let typ = constr_of_Constr (interp_tacarg (evc,env,[],[],Some g,get_debug ())
-    <:tactic<
+  let ist = { evc=evc; env=env; lfun=[]; lmatch=[];
+              goalopt=Some g; debug=get_debug () } in
+  let typ = constr_of_Constr (interp_tacarg ist
+  <:tactic<
       Match Context With
       | [|-(eq ?1 ? ?)] -> ?1
       |	[|-(eqT ?1 ? ?)] -> ?1>>) in
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index e4c852f7f..4e069c11c 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -389,7 +389,7 @@ let inspect n =
              	sp, Lib.Leaf lobj ->
 		  (match sp, object_tag lobj with
                        _, "VARIABLE" ->
-			 let ((_, _, v), _, _) = get_variable sp in
+			 let ((_, _, v), _) = get_variable sp in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
 		     | sp, ("CONSTANT"|"PARAMETER") ->
 			 let {const_type=typ} = Global.lookup_constant sp in
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 6f1be02fb..00259ef99 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -170,7 +170,7 @@ let constant_to_ast_list sp =
       errorlabstrm "print" [< 'sTR "printing of FW terms not implemented" >];;
 
 let variable_to_ast_list sp =
-  let ((id, c, v), _, _) = get_variable sp in
+  let ((id, c, v), _) = get_variable sp in
   let l = implicits_of_var sp in
     (match c with
 	 None -> 
diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v
index 3d29e0503..45ad93aba 100644
--- a/contrib/omega/Zlogarithm.v
+++ b/contrib/omega/Zlogarithm.v
@@ -75,9 +75,8 @@ Definition log_inf_correct1 :=
 Definition log_inf_correct2 := 
 	[p:positive](proj2 ? ? (log_inf_correct p)).
 
-(***TODO: retablir les commandes Opaque / Transparent
 Opaque log_inf_correct1 log_inf_correct2.
-***)
+
 Hints Resolve log_inf_correct1 log_inf_correct2 : zarith.
 
 Lemma log_sup_correct1 : (p:positive)` 0 <= (log_sup p)`.
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 3116bd49b..f4b75583c 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -847,7 +847,7 @@ let print_object lobj id sp dn fv env =
             let hyps = string_list_of_named_context_list hyps in
              print_mutual_inductive packs fv hyps env inner_types
       | "VARIABLE" ->
-          let (_,(varentry,_,_)) = Declare.out_variable lobj in
+          let (_,(varentry,_)) = Declare.out_variable lobj in
            begin
             match varentry with
                Declare.SectionLocalDef body ->