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/ascii_syntax.ml | 2 +-
 plugins/syntax/z_syntax.ml     | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 5c060c3d66..67c9dd0a38 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -37,7 +37,7 @@ let interp_ascii dloc p =
   let rec aux n p =
      if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     GRef (dloc,if Int.equal mp 0 then glob_false else glob_true,None)
+     GRef (dloc,(if Int.equal mp 0 then glob_false else glob_true),None)
      :: (aux (n-1) (p/2)) in
   GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p)
 
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