Merge pull request #119 from math-comp/section-discharge-fight

[hack] section discharge unused

Author: gares

_CoqProject

@@ -51,5 +51,6 @@ tests/type_of_exported_ops.v
 tests/duplicate_structure.v
 tests/instance_params_no_type.v
 tests/test_CS_db_filtering.v
+tests/subtype.v
 
 -R . HB

demo1/hierarchy_1.v

@@ -47,14 +47,14 @@ HB.factory Record Ring_of_TYPE A := {
 
 HB.builders Context A (a : Ring_of_TYPE A).
 
-  Definition to_AddComoid_of_TYPE :=
-    AddComoid_of_TYPE.Build A zero add addrA addrC add0r.
-  HB.instance A to_AddComoid_of_TYPE.
-
-  Definition to_Ring_of_AddComoid :=
-    Ring_of_AddComoid.Build A _ _ _ addNr mulrA mul1r
-      mulr1 mulrDl mulrDr.
-  HB.instance A to_Ring_of_AddComoid.
+HB.instance
+Definition to_AddComoid_of_TYPE :=
+  AddComoid_of_TYPE.Build A zero add addrA addrC add0r.
+
+HB.instance
+Definition to_Ring_of_AddComoid :=
+  Ring_of_AddComoid.Build A _ _ _ addNr mulrA mul1r
+    mulr1 mulrDl mulrDr.
 
 HB.end.
 

demo1/hierarchy_2.v

@@ -32,13 +32,13 @@ HB.factory Record AddAG_of_TYPE A := {
 
 HB.builders Context A (a : AddAG_of_TYPE A).
 
+  HB.instance
   Definition to_AddComoid_of_TYPE :=
     AddComoid_of_TYPE.Build A zero add addrA addrC add0r.
-  HB.instance A to_AddComoid_of_TYPE.
 
+  HB.instance
   Definition to_AddAG_of_AddComoid :=
     AddAG_of_AddComoid.Build A _ addNr.
-  HB.instance A to_AddAG_of_AddComoid.
 
 HB.end.
 HB.structure Definition AddAG := { A of AddAG_of_TYPE A }.
@@ -66,12 +66,12 @@ HB.factory Record Ring_of_AddComoid A of AddComoid A := {
 
 HB.builders Context A (a : Ring_of_AddComoid A).
 
+  HB.instance
   Definition to_AddAG_of_AddComoid := AddAG_of_AddComoid.Build A _ addNr.
-  HB.instance A to_AddAG_of_AddComoid.
 
+  HB.instance
   Definition to_Ring_of_AddAG := Ring_of_AddAG.Build A
     _ _ mulrA mul1r mulr1 mulrDl mulrDr.
-  HB.instance A to_Ring_of_AddAG.
 
 HB.end.
 
@@ -96,9 +96,9 @@ HB.factory Record Ring_of_TYPE A := {
 
 HB.builders Context A (a : Ring_of_TYPE A).
 
+  HB.instance
   Definition to_AddComoid_of_TYPE := AddComoid_of_TYPE.Build A
     zero add addrA addrC add0r.
-  HB.instance A to_AddComoid_of_TYPE.
 
   Definition to_Ring_of_AddComoid := Ring_of_AddComoid.Build A
     _ _ _ addNr mulrA mul1r mulr1 mulrDl mulrDr.

demo2/stage11.v

@@ -306,15 +306,20 @@ HB.mixin Record Join_TAddAG_Uniform T of Uniform_TAddAG_unjoined T := {
   (* TODO: should be subsumed by the type alias TAddAG *)
 HB.factory Record TAddAG_Uniform U of TAddAG_wo_Uniform U := { }.
 
-HB.builders Context U of TAddAG_Uniform U.
-  Definition to_Uniform_wo_Topology : Uniform_wo_Topology U := (TAddAG_uniform _).
-  HB.instance U to_Uniform_wo_Topology.
+HB.builders Context U (a : TAddAG_Uniform U).
+
+  HB.instance
+  Definition to_Uniform_wo_Topology : Uniform_wo_Topology U :=
+    TAddAG_uniform _.
+
+  HB.instance
   Definition to_Join_Uniform_Topology : Join_Uniform_Topology U :=
-    (TAddAG_Join_Uniform_Topology _).
-  HB.instance U to_Join_Uniform_Topology.
-  Definition to_Join_TAddAG_Uniform :=
-    (Join_TAddAG_Uniform.Build U (TAddAG_entourageE _)).
-  HB.instance U to_Join_TAddAG_Uniform.
+    TAddAG_Join_Uniform_Topology _.
+
+  HB.instance
+  Definition to_Join_TAddAG_Uniform : Join_TAddAG_Uniform U :=
+    Join_TAddAG_Uniform.Build U (TAddAG_entourageE _).
+
 HB.end.
 
 HB.structure Definition TAddAG :=
@@ -328,7 +333,7 @@ HB.builders Context T (a : JoinTAddAG T).
   Definition to_JoinTAddAG_wo_Uniform : JoinTAddAG_wo_Uniform T := a.
   HB.instance T to_JoinTAddAG_wo_Uniform.
   (* TODO: Nice error message when factory builders do not depend on the source factory 'a'*)
-  Definition to_Uniform := let _ := a in TAddAG_Uniform.Build T.
+  Definition to_Uniform : TAddAG_Uniform T := let _ := a in TAddAG_Uniform.Build T.
   HB.instance T to_Uniform.
 HB.end.