renamed the coercion

[helm.git] / helm / software / matita / library / legacy / coq.ma

diff --git a/helm/software/matita/library/legacy/coq.ma b/helm/software/matita/library/legacy/coq.ma
index d3c74fe21e88a02b6ab4e502fcf79c669af0bc19..e7a5615d9c633dac55f120e08376fc219e5597cc 100644 (file)
--- a/helm/software/matita/library/legacy/coq.ma
+++ b/helm/software/matita/library/legacy/coq.ma
@@ -14,6 +14,20 @@
 
 set "baseuri" "cic:/matita/legacy/coq/".
 
+default "equality"
+ cic:/Coq/Init/Logic/eq.ind
+ cic:/Coq/Init/Logic/sym_eq.con
+ cic:/Coq/Init/Logic/trans_eq.con
+ cic:/Coq/Init/Logic/eq_ind.con
+ cic:/Coq/Init/Logic/eq_ind_r.con. 
+
+default "true"
+ cic:/Coq/Init/Logic/True.ind. 
+default "false"
+ cic:/Coq/Init/Logic/False.ind. 
+default "absurd"
+ cic:/Coq/Init/Logic/absurd.con. 
+
 (* aritmetic operators *)
 
 interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
@@ -56,3 +70,7 @@ interpretation "Coq's real 'greater than'" 'gt x y = (cic:/Coq/Reals/Rdefinition
 interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y).
 interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)).
 
+interpretation "Coq's natural 'not less or equal than'"
+ 'nleq x y = (cic:/Coq/Init/Logic/not.con 
+               (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y)).
+