aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
authorfilliatr2000-11-02 14:33:31 +0000
committerfilliatr2000-11-02 14:33:31 +0000
commite59113f1bdf4d8c98d956c01f51ae019942d92cd (patch)
treec1ef110c92fbab4112b3e8584e8a8b649f435a70 /pretyping
parentf0a793f123683eaab6bab9968725febe7c311f05 (diff)
suppression des (* open Generic *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml1
-rw-r--r--pretyping/class.ml1
-rwxr-xr-xpretyping/classops.ml1
-rw-r--r--pretyping/coercion.ml1
-rw-r--r--pretyping/detyping.ml1
-rw-r--r--pretyping/evarconv.ml1
-rw-r--r--pretyping/evarutil.ml1
-rw-r--r--pretyping/pretyping.ml1
-rwxr-xr-xpretyping/recordops.ml5
-rwxr-xr-xpretyping/recordops.mli1
-rw-r--r--pretyping/retyping.ml1
-rw-r--r--pretyping/tacred.ml1
-rw-r--r--pretyping/typing.ml1
13 files changed, 0 insertions, 17 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 413ea152a2..84041fb329 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1,7 +1,6 @@
open Util
open Names
-(* open Generic *)
open Term
open Declarations
open Inductive
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 0f201d004f..0ea8e3113a 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -4,7 +4,6 @@
open Util
open Pp
open Names
-(* open Generic *)
open Term
open Inductive
open Declarations
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 36b5ed4d53..249633cbdf 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -9,7 +9,6 @@ open Environ
open Libobject
open Declare
open Term
-(* open Generic *)
open Rawterm
(* usage qque peu general: utilise aussi dans record *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6280fc392b..ad518380dc 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -1,7 +1,6 @@
(* $Id$ *)
open Util
-(* open Generic *)
open Names
open Term
open Reduction
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 70eba2949e..3ed28a91e4 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -5,7 +5,6 @@ open Pp
open Util
open Univ
open Names
-(* open Generic *)
open Term
open Inductive
open Sign
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index fd52e0fa0f..3316e23816 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -3,7 +3,6 @@
open Util
open Names
-(* open Generic *)
open Term
open Reduction
open Instantiate
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ce08a0f390..72e46b52b0 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -5,7 +5,6 @@ open Util
open Pp
open Names
open Univ
-(* open Generic *)
open Term
open Sign
open Environ
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 67e793c54f..5101173308 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -4,7 +4,6 @@
open Pp
open Util
open Names
-(* open Generic *)
open Sign
open Evd
open Term
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f16f77c631..9efd881fac 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -9,11 +9,6 @@ open Typeops
open Libobject
open Library
open Classops
-(*
-open Pp_control
-(* open Generic *)
-open Initial
-*)
let nbimpl = ref 0
let nbpathc = ref 0
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 97c6c53069..8ad0203b35 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -4,7 +4,6 @@
(*i*)
open Names
open Term
-(* open Generic *)
open Classops
open Libobject
open Library
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 53bf5b08a7..22eba722cc 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -5,7 +5,6 @@ open Util
open Term
open Inductive
open Names
-(* open Generic *)
open Reduction
open Environ
open Typeops
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 77f8cf9e11..653a08fdc0 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -4,7 +4,6 @@
open Pp
open Util
open Names
-(* open Generic *)
open Term
open Inductive
open Environ
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 23028cc626..3f0ab9501a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -3,7 +3,6 @@
open Util
open Names
-(* open Generic *)
open Term
open Environ
open Reduction