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 /plugins/micromega | |
| parent | 9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff) | |
Removing dead code and unused opens.
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 2 | ||||
| -rw-r--r-- | plugins/micromega/g_micromega.ml4 | 5 |
2 files changed, 0 insertions, 7 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 5fef6d3fc6..5c0a8226a7 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -18,9 +18,7 @@ open Pp open Mutils -open Proofview open Goptions -open Proofview.Notations (** * Debug flag diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index bca1c2febd..e6b5cc60d4 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -16,12 +16,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Errors -open Misctypes -open Stdarg open Constrarg -open Pcoq.Prim -open Pcoq.Tactic DECLARE PLUGIN "micromega_plugin" |