From b20e1be71f9b5c5585b214e30b5042676fa6cd46 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Fri, 29 Dec 2000 19:23:25 +0000
Subject: 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
---
 library/declare.ml  | 1 +
 library/declare.mli | 3 ++-
 2 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'library')

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
 
-- 
cgit v1.2.3