diff options
Diffstat (limited to 'checker/subtyping.ml')
| -rw-r--r-- | checker/subtyping.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 7d2ced7fd..390c2b9e7 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -18,9 +18,6 @@ open Reduction open Inductive open Modops (*i*) -open Pp - - (* This local type is used to subtype a constant with a constructor or an inductive type. It can also be useful to allow reorderings in |