4 files changed, 21 insertions, 21 deletions
diff --git a/src/nbe/Data.ml b/src/nbe/Data.ml
index 8589ea5..38739b3 100644
--- a/src/nbe/Data.ml
+++ b/src/nbe/Data.ml
@@ -2,11 +2,11 @@ open Bwd
 
 type syn =
   | Var of int
-  | Def of Ident.t * value Lazy.t
-  | Pi of Ident.local * syn * (* BINDS *) syn
-  | Lam of Ident.local * (* BINDS *) syn
+  | Def of Name.t * value Lazy.t
+  | Pi of Name.local * syn * (* BINDS *) syn
+  | Lam of Name.local * (* BINDS *) syn
   | App of syn * syn
-  | Sg of Ident.local * syn * (* BINDS *) syn
+  | Sg of Name.local * syn * (* BINDS *) syn
   | Pair of syn * syn
   | Fst of syn
   | Snd of syn
@@ -15,7 +15,7 @@ type syn =
   | True
   | False
   | BoolElim of {
-      motive_var : Ident.local;
+      motive_var : Name.local;
       motive : (* BINDS *) syn;
       true_case : syn;
       false_case : syn;
@@ -25,9 +25,9 @@ type syn =
 and value =
   | Neutral of ne
   | Unfold of unfold
-  | Pi of Ident.local * value * clo
-  | Lam of Ident.local * clo
-  | Sg of Ident.local * value * clo
+  | Pi of Name.local * value * clo
+  | Lam of Name.local * clo
+  | Sg of Name.local * value * clo
   | Pair of value * value
   | Type
   | Bool
@@ -40,14 +40,14 @@ and ne_head =
 
 and unfold = unfold_head * frm bwd * value Lazy.t
 and unfold_head =
-  | Def of Ident.t * value Lazy.t
+  | Def of Name.t * value Lazy.t
 
 and frm = 
   | App of value
   | Fst
   | Snd
   | BoolElim of {
-      motive_var : Ident.local;
+      motive_var : Name.local;
       motive: clo;
       true_case: value;
       false_case: value;
diff --git a/src/nbe/Domain.ml b/src/nbe/Domain.ml
index bf5ed90..f0922e8 100644
--- a/src/nbe/Domain.ml
+++ b/src/nbe/Domain.ml
@@ -3,9 +3,9 @@ open Bwd
 type t = Data.value =
   | Neutral of ne
   | Unfold of unfold
-  | Pi of Ident.local * t * clo
-  | Lam of Ident.local * clo
-  | Sg of Ident.local * t * clo
+  | Pi of Name.local * t * clo
+  | Lam of Name.local * clo
+  | Sg of Name.local * t * clo
   | Pair of t * t
   | Type
   | Bool
@@ -18,14 +18,14 @@ and ne_head = Data.ne_head =
 
 and unfold = Data.unfold
 and unfold_head = Data.unfold_head =
-  | Def of Ident.t * t Lazy.t
+  | Def of Name.t * t Lazy.t
 
 and frm = Data.frm =
   | App of t
   | Fst
   | Snd
   | BoolElim of {
-      motive_var : Ident.local;
+      motive_var : Name.local;
       motive : clo;
       true_case : t;
       false_case: t;
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;
diff --git a/src/nbe/dune b/src/nbe/dune
index 3e62347..184d44f 100644
--- a/src/nbe/dune
+++ b/src/nbe/dune
@@ -1,4 +1,4 @@
 (library
  (name NbE)
  (public_name toytt.nbe)
- (libraries algaeff bwd toytt.ident toytt.error))
+ (libraries algaeff bwd toytt.error toytt.name))