nouvel algo de conversion plus uniforme

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

6 files changed, 6 insertions, 0 deletions

diff --git a/contrib/correctness/peffect.ml b/contrib/correctness/peffect.ml
index 23d4dea344..1db31269b9 100644
--- a/contrib/correctness/peffect.ml
+++ b/contrib/correctness/peffect.ml
@@ -11,6 +11,7 @@
 (* $Id$ *)
 
 open Names
+open Nameops
 open Pmisc
 
 (* The type of effects.
diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index feee251ff5..c3cc1ec64a 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -14,6 +14,7 @@ open Pmisc
 open Past
 open Ptype
 open Names
+open Nameops
 open Libobject
 open Library
 open Term
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 452e1b5811..17c673a543 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -13,6 +13,7 @@
 open Pp
 open Util
 open Names
+open Nameops
 open Term
 open Himsg
 
diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml
index 6824632382..122ff16ab5 100644
--- a/contrib/correctness/prename.ml
+++ b/contrib/correctness/prename.ml
@@ -11,6 +11,7 @@
 (* $Id$ *)
 
 open Names
+open Nameops
 open Util
 open Pp
 open Himsg
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 77d2616532..6b487348a8 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -14,6 +14,7 @@
 
 open Options
 open Names
+open Nameops
 open Vernacentries
 open Reduction
 open Term
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index fecd577d7c..5e454a2520 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -12,6 +12,7 @@
 
 open Util
 open Names
+open Nameops
 open Term
 open Termops
 open Pattern