From 66cf5d3c5fff84a1cac333c1aa81a8e1f21ee6f4 Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Mon, 8 Jul 2024 22:10:12 +0200
Subject: rename Ident -> Name

---
 src/nbe/Syntax.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'src/nbe/Syntax.ml')

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;
-- 
cgit 1.4.1