X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fre%2Flang.ma;h=9f40045aee9b6b923e0c911078066c5f8b6d0ef8;hb=45ab745cdc286db123f9811adef343c9178c28de;hp=7424522c7fcb00a784431ca666e85e8c8f44e2f0;hpb=bc477154d15f6979c948f9af602199af547d193e;p=helm.git

diff --git a/matita/matita/lib/re/lang.ma b/matita/matita/lib/re/lang.ma
index 7424522c7..9f40045ae 100644
--- a/matita/matita/lib/re/lang.ma
+++ b/matita/matita/lib/re/lang.ma
@@ -34,7 +34,7 @@ let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝
 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
 
 let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
-match l with [ nil ⇒ ⊤ | cons w tl ⇒ r w ∧ conjunct ? tl r ]. 
+match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ]. 
 
 (* kleene's star *)
 definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l.