diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 038bf465a..204f506a6 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -12,7 +12,6 @@ open Context open Declarations open Environ open Evd -open Sign (** The following three functions are similar to the ones defined in Inductive, but they expect an env *) |