Merge pull request #572 from cecilemarcon/fixhowto

Fix HB.howto infinite loop

Author: CohenCyril

HB/common/database.elpi

@@ -230,9 +230,9 @@ findall-mixin-src T ML :-
 func findall-factory->constructor -> list prop.
 findall-factory->constructor L :-
   std.map {std.findall (findall-factory->constructor.aux _)} findall-factory->constructor.make L.
-func findall-factory->constructor.aux -> prop.
+pred findall-factory->constructor.aux o:prop.
 findall-factory->constructor.aux (factory->constructor F C) :-
-  is-factory F, !, factory->constructor F C.
+  is-factory F, factory->constructor F C.
 func findall-factory->constructor.make prop -> prop.
 findall-factory->constructor.make (findall-factory->constructor.aux P) P.
 

_CoqProject.test-suite

@@ -22,6 +22,7 @@ examples/demo5/hierarchy_0.v
 # examples/cat/cat.v
 examples/cat/cat.v
 
+tests/test_howto.v
 tests/type_of_exported_ops.v
 tests/duplicate_structure.v
 tests/instance_params_no_type.v

tests/test_howto.v

@@ -0,0 +1,7 @@
+From HB Require Import structures.
+
+HB.mixin Record hasB T := Mixin { b : unit; }.
+HB.mixin Record hasA T := Mixin { a : bool; }.
+HB.structure Definition A := { T of hasA T}.
+
+HB.howto A.type.  (* runs forever *)