aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/xml/xmlcommand.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 4aa22a71b..a653b1c04 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -77,7 +77,8 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *)
match tag with
"CONSTANT" ->
(match D.constant_strength sp with
- D.DischargeAt _ -> false (* a local definition *)
+ | D.DischargeAt _ -> false (* a local definition *)
+ | D.NotDeclare -> false (* not a definition *)
| D.NeverDischarge -> true (* a non-local one *)
)
| "PARAMETER" (* axioms and *)