Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / model / abgroups / Qposabgroup.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/Qposabgroup.mma b/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/Qposabgroup.mma
index 161364874c4ab29bde1a0237a6a4a5c1f243ace3..de1f956029423af3602b0659fa145a2d1c283e35 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/Qposabgroup.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/model/abgroups/Qposabgroup.mma
@@ -26,7 +26,7 @@ include "algebra/CAbGroups.ma".
 The positive rationals form with the multiplication a CAbgroup.
 *)
 
-inline procedural "cic:/CoRN/model/abgroups/Qposabgroup/Qpos_mult_is_CAbGroup.con".
+inline procedural "cic:/CoRN/model/abgroups/Qposabgroup/Qpos_mult_is_CAbGroup.con" as definition.
 
-inline procedural "cic:/CoRN/model/abgroups/Qposabgroup/Qpos_mult_as_CAbGroup.con".
+inline procedural "cic:/CoRN/model/abgroups/Qposabgroup/Qpos_mult_as_CAbGroup.con" as definition.