From 85250f99c8a0edee3469d1370e6b39c9a0c88f4b Mon Sep 17 00:00:00 2001
From: hondet <hondet@nancy.private.lsv.fr>
Date: Tue, 20 Oct 2020 18:08:10 +0200
Subject: [PATCH] removed refl builtin from prelude

---
 prelude/logic.lp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/prelude/logic.lp b/prelude/logic.lp
index 856bce4..6694784 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -87,7 +87,6 @@ proof
 admit
 
 constant symbol reflexivity_of_equals: Prf (∀B (λt, ∀ (λx: El t, x = x)))
-set builtin "refl" ≔ reflexivity_of_equals
 
 constant
 symbol transitivity_of_equals
-- 
GitLab