added do_heavy_checks default

[helm.git] / helm / software / matita / dama / excedence.ma

diff --git a/helm/software/matita/dama/excedence.ma b/helm/software/matita/dama/excedence.ma
index 1bddcb16eabdc9876b0c3219650de8a176485b3d..fa6848e120314b987eaa0f61bf81cec57d42dea6 100644 (file)
--- a/helm/software/matita/dama/excedence.ma
+++ b/helm/software/matita/dama/excedence.ma
@@ -52,7 +52,7 @@ record apartness : Type ≝ {
 }.
 
 notation "a break # b" non associative with precedence 50 for @{ 'apart $a $b}.
-interpretation "axiomatic apartness" 'apart x y = 
+interpretation "apartness" 'apart x y = 
   (cic:/matita/excedence/ap_apart.con _ x y).
 
 definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y.