Procedural: explicit flavour specification for constants is now working

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

diff --git a/helm/software/matita/contribs/CoRN-Procedural/model/groups/Qposgroup.mma b/helm/software/matita/contribs/CoRN-Procedural/model/groups/Qposgroup.mma
index 90d5b8419b20ab3579a859c79392cd33ec46deb3..00cc590adcf3a52ac0f42e6446ad6c8f1d91bb70 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Procedural/model/groups/Qposgroup.mma
+++ b/helm/software/matita/contribs/CoRN-Procedural/model/groups/Qposgroup.mma
@@ -26,7 +26,7 @@ include "algebra/CGroups.ma".
 The positive rational numbers form a multiplicative group.
 *)
 
-inline procedural "cic:/CoRN/model/groups/Qposgroup/Qpos_is_CGroup.con".
+inline procedural "cic:/CoRN/model/groups/Qposgroup/Qpos_is_CGroup.con" as lemma.
 
-inline procedural "cic:/CoRN/model/groups/Qposgroup/Qpos_as_CGroup.con".
+inline procedural "cic:/CoRN/model/groups/Qposgroup/Qpos_as_CGroup.con" as definition.