Small bugfix with "not".

picnic · Oct 8, 2012 · 9a43046 · 9a43046
1 parent 31e13b6
commit 9a43046
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/host2spec.ml b/host2spec.ml
@@ -244,7 +244,7 @@ let isNot constr =
     let str' = try let i = String.rindex str '#' in
       String.sub str (i+1) (String.length str - i - 1)
     with Not_found | Invalid_argument _ -> str in
-    str' = "not"
+    str' = "not" || str' = "Coq.Init.Logic.not"
   else false
 
 (* Parses a premisse of a predicate's constructor (or property). *)