From 99cda3324ad90fc77e810f0412f44bf81df99371 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 21 Apr 2000 22:09:59 +0000
Subject: discharge des axiomes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@366 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml  | 3 +++
 library/declare.mli | 1 +
 2 files changed, 4 insertions(+)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 5e87c1a749..51748a0204 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -189,6 +189,9 @@ let is_constant sp =
 let constant_strength sp = 
   let (_,stre) = Spmap.find sp !csttab in stre
 
+let constant_or_parameter_strength sp =
+  try constant_strength sp with Not_found -> NeverDischarge
+
 let is_variable id = 
   let sp = Nametab.sp_of_id CCI id in Spmap.mem sp !vartab
   
diff --git a/library/declare.mli b/library/declare.mli
index 8541c20921..470d6dee9d 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -43,6 +43,7 @@ val make_strength_2 : unit -> strength
 
 val is_constant : section_path -> bool
 val constant_strength : section_path -> strength
+val constant_or_parameter_strength : section_path -> strength
 
 val is_variable : identifier -> bool
 val out_variable : 
-- 
cgit v1.2.3