From a77bca84565b26aeedec3b210d761240d9d261f4 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 5 Dec 2013 07:55:11 +0100
Subject: Imported Upstream version 0.4

---
 coq.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'coq.ml')

diff --git a/coq.ml b/coq.ml
index 7371913..132fbf7 100644
--- a/coq.ml
+++ b/coq.ml
@@ -148,6 +148,8 @@ module Leibniz = struct
   let path = ["Coq"; "Init"; "Logic"]
   let eq_refl = lazy (init_constant path "eq_refl")
   let eq_refl ty x = lapp eq_refl [| ty;x|]
+  let eq ty = Term.mkApp (init_constant path "eq", [| ty |])
+
 end
 
 module Option = struct
-- 
cgit v1.2.3