diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-08 18:59:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-08 19:59:03 +0200 |
| commit | f461e7657cab9917c5b405427ddba3d56f197efb (patch) | |
| tree | 467ac699f78d0360b05174238aeb1177da892503 /printing/printmod.ml | |
| parent | 9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff) | |
Removing dead code and unused opens.
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 9354cd28d..5f98eeeab 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -65,7 +65,6 @@ let get_new_id locals id = (** Inductive declarations *) -open Termops open Reduction let print_params env sigma params = |