Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / matita / contribs / CoRN-Procedural / model / groups / Qgroup.mma

diff --git a/helm/software/matita/contribs/CoRN-Procedural/model/groups/Qgroup.mma b/helm/software/matita/contribs/CoRN-Procedural/model/groups/Qgroup.mma
index 9398c0626e97bcda07b2d03cf56f6688a445e7e7..080e86fad83583b6c9bf837602b89f4ce513b25c 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/model/groups/Qgroup.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/model/groups/Qgroup.mma
@@ -26,7 +26,7 @@ include "algebra/CGroups.ma".
 The rational numbers with addition form a group. The inverse function is taking the opposite.
 *)
 
-inline procedural "cic:/CoRN/model/groups/Qgroup/Q_is_CGroup.con".
+inline procedural "cic:/CoRN/model/groups/Qgroup/Q_is_CGroup.con" as lemma.
 
-inline procedural "cic:/CoRN/model/groups/Qgroup/Q_as_CGroup.con".
+inline procedural "cic:/CoRN/model/groups/Qgroup/Q_as_CGroup.con" as definition.