diff options
| author | Pierre-Marie Pédrot | 2016-05-08 18:59:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-08 19:59:03 +0200 |
| commit | f461e7657cab9917c5b405427ddba3d56f197efb (patch) | |
| tree | 467ac699f78d0360b05174238aeb1177da892503 /toplevel | |
| parent | 9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff) | |
Removing dead code and unused opens.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 1 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 1 | ||||
| -rw-r--r-- | toplevel/record.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 1 |
6 files changed, 0 insertions, 6 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 38bc0e568e..5865fec060 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -13,7 +13,6 @@ open Flags open Term open Vars open Termops -open Entries open Environ open Redexpr open Declare diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 04182cf236..c6f49dcd48 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -9,7 +9,6 @@ open Pp open Errors open Util -open System open Flags open Names open Libnames diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index ffa11679c2..6b267283a4 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -11,7 +11,6 @@ open Errors open Util open Term open Vars -open Entries open Declarations open Cooking open Entries diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a041ee620c..701bc5da54 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -23,7 +23,6 @@ open Vernacexpr open Pcoq open Libnames open Tok -open Egramml open Egramcoq open Notation open Nameops diff --git a/toplevel/record.ml b/toplevel/record.ml index 93429da5ac..d12b5ee8e4 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -26,7 +26,6 @@ open Constrexpr_ops open Goptions open Sigma.Notations open Context.Rel.Declaration -open Entries (********** definition d'un record (structure) **************) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 89bc31d0ac..1c8d602517 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -12,7 +12,6 @@ open Pp open Errors open Util open Flags -open System open Vernacexpr (* The functions in this module may raise (unexplainable!) exceptions. |