From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 1 Dec 2008 15:37:28 +0000 (+0000)
Subject: we start a kernel for the version "basic with reverse indexes and global
X-Git-Tag: make_still_working~4469
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b0f7c07bc4115c795f17ac319ee795a6d8118b22;p=helm.git

we start a kernel for the version "basic with reverse indexes and global
references"
---

diff --git a/helm/software/lambda-delta/.depend.opt b/helm/software/lambda-delta/.depend.opt
index 60e0390bd..4ad04534d 100644
--- a/helm/software/lambda-delta/.depend.opt
+++ b/helm/software/lambda-delta/.depend.opt
@@ -8,6 +8,8 @@ automath/autParser.cmo: automath/aut.cmx automath/autParser.cmi
 automath/autParser.cmx: automath/aut.cmx automath/autParser.cmi 
 automath/autLexer.cmo: automath/autParser.cmi 
 automath/autLexer.cmx: automath/autParser.cmx 
+basic_rg/brg.cmo: lib/nUri.cmi automath/aut.cmx 
+basic_rg/brg.cmx: lib/nUri.cmx automath/aut.cmx 
 toplevel/meta.cmo: lib/nUri.cmi automath/aut.cmx 
 toplevel/meta.cmx: lib/nUri.cmx automath/aut.cmx 
 toplevel/metaOutput.cmi: toplevel/meta.cmx 
diff --git a/helm/software/lambda-delta/Makefile b/helm/software/lambda-delta/Makefile
index 50f1a83b6..e7aa0ae76 100644
--- a/helm/software/lambda-delta/Makefile
+++ b/helm/software/lambda-delta/Makefile
@@ -1,6 +1,6 @@
 MAIN = helena
 
-DIRECTORIES = lib automath toplevel
+DIRECTORIES = lib automath basic_rg toplevel
 
 REQUIRES = unix
 
diff --git a/helm/software/lambda-delta/basic_rg/Make b/helm/software/lambda-delta/basic_rg/Make
new file mode 100644
index 000000000..be843055b
--- /dev/null
+++ b/helm/software/lambda-delta/basic_rg/Make
@@ -0,0 +1 @@
+brg
diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml
new file mode 100644
index 000000000..a3a32f8d0
--- /dev/null
+++ b/helm/software/lambda-delta/basic_rg/brg.ml
@@ -0,0 +1,15 @@
+module U = NUri
+module A = Aut
+
+type uri = U.uri
+type id = A.id
+
+type binder = Abst | Abbr
+
+type term = Sort of int
+          | LRef of int
+	  | GRef of uri
+	  | Cast of term * term
+	  | Appl of term * term
+	  | Bind of id * binder * term * term
+