X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Fkernel.ml;fp=matita%2Fcomponents%2Fbinaries%2Fmatex%2Fkernel.ml;h=818ad07d9e9319c013e990f576f3f60ca1d5bb60;hb=f462726eaf4edb5852851ec5d265cdafe9d3a78d;hp=8b6a81a3e64d110e40eba37072d2e491054e318d;hpb=ffc3e681a82dc32269cc87407a95db6c922d3bfb;p=helm.git

diff --git a/matita/components/binaries/matex/kernel.ml b/matita/components/binaries/matex/kernel.ml
index 8b6a81a3e..818ad07d9 100644
--- a/matita/components/binaries/matex/kernel.ml
+++ b/matita/components/binaries/matex/kernel.ml
@@ -46,9 +46,11 @@ let init () =
    let u1 = mk_type_universe "1" in
    E.add_lt_constraint ~acyclic:true u0 u1
 
-let fst_var = 1
+let fst_var = 1 (* first variable *)
 
-let snd_var = 2
+let snd_var = 2 (* second variable *)
+
+let fst_con = 1 (* first constructor *)
 
 let appl ts = C.Appl ts