nouvel algo de conversion plus uniforme

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

4 files changed, 8 insertions, 94 deletions

diff --git a/library/nameops.ml b/library/nameops.ml
index b7609bafde..0bcaeffbc1 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -8,6 +8,7 @@
 
 (* $Id$ *)
 
+open Pp
 open Util
 open Names
 open Declarations
@@ -16,6 +17,8 @@ open Term
 
 (* Identifiers *)
 
+let pr_id id = [< 'sTR (string_of_id id) >]
+
 let wildcard = id_of_string "_"
 
 (* Utilities *)
@@ -141,6 +144,9 @@ let next_name_away name l =
     | Anonymous -> id_of_string "_"
 
 (**********************************************)
+
+let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >]
+
 (* Operations on dirpaths *)
 let empty_dirpath = make_dirpath []
 
diff --git a/library/nameops.mli b/library/nameops.mli
index fc5bc6a6a8..b0376723b5 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -13,6 +13,7 @@ open Term
 open Environ
 
 (* Identifiers and names *)
+val pr_id : identifier -> Pp.std_ppcmds
 val wildcard : identifier
 
 val make_ident : string -> int option -> identifier
@@ -34,6 +35,7 @@ val next_name_away_with_default :
 val out_name : name -> identifier
 
 (* Section and module mechanism: dealinng with dir paths *)
+val pr_dirpath : dir_path -> Pp.std_ppcmds
 val empty_dirpath : dir_path
 val default_module : dir_path
 
diff --git a/library/opaque.ml b/library/opaque.ml
deleted file mode 100644
index ff551ce557..0000000000
--- a/library/opaque.ml
+++ /dev/null
@@ -1,64 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ *)
-
-(*i*)
-open Util
-open Pp
-open Names
-open Closure
-open Summary
-open Term
-open Declarations
-(*i*)
-
-let tr_state = ref all_transparent
-
-let state () = !tr_state
-
-let _ = 
-  declare_summary "Transparent constants and variables"
-    { freeze_function = state;
-      unfreeze_function = (fun ts -> tr_state := ts);
-      init_function = (fun () -> tr_state := all_transparent);
-      survive_section = false }
-
-let is_evaluable env ref =
-  match ref with
-      EvalConstRef sp ->
-        let (ids,sps) = !tr_state in
-        Sppred.mem sp sps &
-        let cb = Environ.lookup_constant sp env in
-        cb.const_body <> None & not cb.const_opaque
-    | EvalVarRef id ->
-        let (ids,sps) = !tr_state in
-        Idpred.mem id ids &
-        let (_,value,_) = Environ.lookup_named id env in
-        value <> None
-
-(* Modifying this state *)
-let set_opaque_const sp =
-  let (ids,sps) = !tr_state in
-  tr_state := (ids, Sppred.remove sp sps)
-let set_transparent_const sp =
-  let (ids,sps) = !tr_state in
-  let cb = Global.lookup_constant sp in
-  if cb.const_body <> None & cb.const_opaque then
-    errorlabstrm "set_transparent_const"
-      [< 'sTR "Cannot make"; 'sPC; 
-	 Nametab.pr_global_env (Global.env()) (Nametab.ConstRef sp);
-	 'sPC; 'sTR "transparent because it was declared opaque." >];
-  tr_state := (ids, Sppred.add sp sps)
-
-let set_opaque_var id =
-  let (ids,sps) = !tr_state in
-  tr_state := (Idpred.remove id ids, sps)
-let set_transparent_var id =
-  let (ids,sps) = !tr_state in
-  tr_state := (Idpred.add id ids, sps)
diff --git a/library/opaque.mli b/library/opaque.mli
deleted file mode 100644
index 7277cb66f8..0000000000
--- a/library/opaque.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Names
-open Closure
-open Safe_typing
-open Environ
-(*i*)
-
-(* The current set of transparent constants and variables *)
-val state : unit -> transparent_state
-
-(* returns true if the global reference has a definition and that is
-   has not been set opaque *)
-val is_evaluable : env -> evaluable_global_reference -> bool
-
-(* Modifying this state *)
-val set_opaque_const : section_path -> unit
-val set_transparent_const : section_path -> unit
-
-val set_opaque_var : identifier -> unit
-val set_transparent_var : identifier -> unit