1 files changed, 5 insertions, 5 deletions
diff --git a/src/nbe/Syntax.ml b/src/nbe/Syntax.ml
index 5de5281..859102a 100644
--- a/src/nbe/Syntax.ml
+++ b/src/nbe/Syntax.ml
@@ -1,10 +1,10 @@
 type t = Data.syn =
   | Var of int
-  | Def of Ident.t * Data.value Lazy.t
-  | Pi of Ident.local * t * (* BINDS *) t
-  | Lam of Ident.local * (* BINDS *) t
+  | Def of Name.t * Data.value Lazy.t
+  | Pi of Name.local * t * (* BINDS *) t
+  | Lam of Name.local * (* BINDS *) t
   | App of t * t
-  | Sg of Ident.local * t * (* BINDS *) t
+  | Sg of Name.local * t * (* BINDS *) t
   | Pair of t * t
   | Fst of t
   | Snd of t
@@ -13,7 +13,7 @@ type t = Data.syn =
   | True
   | False
   | BoolElim of {
-      motive_var : Ident.local;
+      motive_var : Name.local;
       motive : (* BINDS *) t;
       true_case : t;
       false_case : t;