diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-29 19:23:25 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-29 19:23:25 +0000 |
| commit | b20e1be71f9b5c5585b214e30b5042676fa6cd46 (patch) | |
| tree | 6e9b6b6078d69420ee90751377d2f015fd8f1323 /library | |
| parent | 50457d3bf6aee2a49dd9c0acf7389b885178ea3f (diff) | |
Ajout du Let pour le langage de tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
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 621666d67..123cbd188 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 3c5e99608..b902be207 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 |