diff options
Diffstat (limited to 'pretyping/classops.ml')
| -rwxr-xr-x | pretyping/classops.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 36b5ed4d53..249633cbdf 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -9,7 +9,6 @@ open Environ open Libobject open Declare open Term -(* open Generic *) open Rawterm (* usage qque peu general: utilise aussi dans record *) |