From 57bee17f928fc67a599d2116edb42a59eeb21477 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 11 Oct 2013 18:30:54 +0200
Subject: Rework handling of universes on top of the STM, allowing for delayed
 computation in case of non-polymorphic proofs. Also fix plugins after
 forgotten merge conflicts. Still does not compile everything.

---
 plugins/syntax/z_syntax.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/syntax/z_syntax.ml')

diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 5131a5f38e..2b1410be67 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -182,8 +182,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binnums)
   z_of_int
-  ([GRef (Loc.ghost, glob_ZERO, None, None);
-    GRef (Loc.ghost, glob_POS, None, None);
-    GRef (Loc.ghost, glob_NEG, None, None)],
+  ([GRef (Loc.ghost, glob_ZERO, None);
+    GRef (Loc.ghost, glob_POS, None);
+    GRef (Loc.ghost, glob_NEG, None)],
   uninterp_z,
   true)
-- 
cgit v1.2.3