diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 1 | ||||
| -rw-r--r-- | library/declare.mli | 3 |
2 files changed, 3 insertions, 1 deletions
diff --git a/library/declare.ml b/library/declare.ml index 621666d677..123cbd188f 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -17,6 +17,7 @@ open Impargs open Indrec type strength = + | NotDeclare | DischargeAt of dir_path | NeverDischarge diff --git a/library/declare.mli b/library/declare.mli index 3c5e996089..b902be207b 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -16,7 +16,8 @@ open Inductive reset works properly --- and will fill some global tables such as [Nametab] and [Impargs]. *) -type strength = +type strength = + | NotDeclare | DischargeAt of dir_path | NeverDischarge |