]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brg.ml
autItem : the uris of the objects involved in the implicit coercions
[helm.git] / helm / software / lambda-delta / basic_rg / brg.ml
index 4778e5c3e9ef8716a46ccff050ecb211eef90eda..73da25b2db4628f6046df0f010a6e5008e06bcdd 100644 (file)
@@ -43,6 +43,10 @@ let appl u t = Appl (u, t)
 
 let bind id b t = Bind (id, b, t)
 
+let bind_abst id u t = Bind (id, Abst u, t)
+
+let bind_abbr id v t = Bind (id, Abbr v, t)
+
 (* context handling functions ***********************************************)
 
 let empty_context = 0, []