aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
authorfilliatr2000-11-02 14:33:31 +0000
committerfilliatr2000-11-02 14:33:31 +0000
commite59113f1bdf4d8c98d956c01f51ae019942d92cd (patch)
treec1ef110c92fbab4112b3e8584e8a8b649f435a70 /proofs
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 'proofs')
-rw-r--r--proofs/clenv.ml1
-rw-r--r--proofs/evar_refiner.ml1
-rw-r--r--proofs/logic.ml1
-rw-r--r--proofs/pfedit.ml1
-rw-r--r--proofs/refiner.ml1
-rw-r--r--proofs/tacinterp.ml1
-rw-r--r--proofs/tacmach.ml1
7 files changed, 0 insertions, 7 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 726042c356..962073127d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -4,7 +4,6 @@
open Pp
open Util
open Names
-(* open Generic *)
open Term
open Sign
open Instantiate
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index efeda72f38..7a9dbb1772 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -5,7 +5,6 @@ open Pp
open Util
open Stamps
open Names
-(* open Generic *)
open Term
open Environ
open Evd
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2bf95aed11..17eff5195f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -5,7 +5,6 @@ open Pp
open Util
open Names
open Evd
-(* open Generic *)
open Term
open Sign
open Environ
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 62629a65bb..be84461012 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -5,7 +5,6 @@ open Pp
open Util
open Names
open Sign
-(* open Generic *)
open Term
open Declarations
open Environ
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 6a40e2c9d7..1942b42649 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -4,7 +4,6 @@
open Pp
open Util
open Stamps
-(* open Generic *)
open Term
open Sign
open Evd
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 98f2b35545..09dc5a0955 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -4,7 +4,6 @@
open Astterm
open Closure
open Dyn
-(* open Generic *)
open Libobject
open Pattern
open Pp
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 4b2fcbc8ef..6e0fafd8a0 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -4,7 +4,6 @@
open Util
open Stamps
open Names
-(* open Generic *)
open Sign
open Term
open Instantiate