Scripts fixed. They were broken since the change to the behaviour of CicMetaSubst...

[helm.git] / helm / software / matita / library / algebra / CoRN / SemiGroups.ma

diff --git a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
index f57e7c41ab7cedfe9884c4056a19ee94898b9d6f..b57d3b2fde5f22d2a735e277df8be2f35090d085 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
+++ b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
@@ -269,10 +269,10 @@ definition dprod: \forall M1,M2:CSemiGroup. \forall x:ProdCSetoid (csg_crr M1) (
   \lambda M1,M2:CSemiGroup. \lambda x:ProdCSetoid (csg_crr M1) (csg_crr M2).
   \lambda y:ProdCSetoid (csg_crr M1) (csg_crr M2).
   match x with 
-    [pairT (x1: (cs_crr (csg_crr M1))) (x2: (cs_crr (csg_crr M2))) \Rightarrow 
+    [pair (x1: (cs_crr (csg_crr M1))) (x2: (cs_crr (csg_crr M2))) \Rightarrow 
      match y with 
-       [pairT (y1: (cs_crr (csg_crr M1))) (y2: (cs_crr (csg_crr M2))) \Rightarrow 
-          pairT (cs_crr (csg_crr M1)) (cs_crr (csg_crr M2))
+       [pair (y1: (cs_crr (csg_crr M1))) (y2: (cs_crr (csg_crr M2))) \Rightarrow 
+          pair (cs_crr (csg_crr M1)) (cs_crr (csg_crr M2))
 (csbf_fun ? ? ? (csg_op M1) x1 y1) (csbf_fun ? ? ? (csg_op M2) x2 y2)]].
 
 lemma dprod_strext: \forall M1,M2:CSemiGroup.