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