Merge pull request #375 from math-comp/name-main

name main rule

Author: CohenCyril

structures.v

@@ -251,6 +251,7 @@ Elpi Accumulate Db hb.db.
    can save a few (2 or 3) percents of total compilation time on MathComp. *)
 Elpi Accumulate lp:{{
 
+:name "start"
 main [str S] :- !,
   if (decl-location {coq.locate S} Loc)
      (coq.say "HB: synthesized in file" Loc)
@@ -286,6 +287,7 @@ Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate File "HB/about.elpi".
 Elpi Accumulate lp:{{
 
+:name "start"
 main [str S] :- !, with-attributes (with-logging (about.main S)).
 
 main _ :- coq.error "Usage: HB.about <name>.".
@@ -320,6 +322,7 @@ Elpi Accumulate File "HB/about.elpi".
 Elpi Accumulate File "HB/howto.elpi".
 Elpi Accumulate lp:{{
 
+:name "start"
 main [trm T, str STgt] :- !,
   with-attributes (with-logging (howto.main-trm T STgt none)).
 main [trm T, str STgt, int Depth] :- !,
@@ -359,6 +362,7 @@ Elpi Accumulate File "HB/common/utils.elpi".
 Elpi Accumulate File "HB/status.elpi".
 Elpi Accumulate lp:{{
 
+:name "start"
 main [] :- !, status.print-hierarchy.
 
 main _ :- coq.error "Usage: HB.status.".
@@ -388,6 +392,7 @@ Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate File "HB/graph.elpi".
 Elpi Accumulate lp:{{
 
+:name "start"
 main [str File] :- with-attributes (with-logging (graph.to-file File)).
 main _ :- coq.error "Usage: HB.graph <filename>.".
 
@@ -441,6 +446,7 @@ Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate File "HB/factory.elpi".
 Elpi Accumulate lp:{{
 
+:name "start"
 main [A] :- A = indt-decl _, !,
   with-attributes (with-logging (factory.declare-mixin A)).
 
@@ -498,6 +504,7 @@ Elpi Accumulate File "HB/common/synthesis.elpi".
 Elpi Accumulate File "HB/pack.elpi".
 Elpi Accumulate lp:{{
 
+:name "start"
 solve (goal _ _ S _ [trm Ty | Args] as G) GLS :- with-attributes (with-logging (std.do! [
   pack.main Ty Args InstanceSkel,
   std.assert-ok! (coq.elaborate-skeleton InstanceSkel S Instance) "HB.pack_for: the instance does not solve the goal",
@@ -520,6 +527,7 @@ Elpi Accumulate File "HB/common/synthesis.elpi".
 Elpi Accumulate File "HB/pack.elpi".
 Elpi Accumulate lp:{{
 
+:name "start"
 solve (goal _ _ Ty _ Args as G) GLS :- with-attributes (with-logging (std.do! [
   pack.main Ty Args InstanceSkel,
   std.assert-ok! (coq.elaborate-skeleton InstanceSkel Ty Instance) "HB.pack: the instance does not solve the goal",
@@ -608,6 +616,7 @@ Elpi Accumulate File "HB/factory.elpi".
 Elpi Accumulate File "HB/structure.elpi".
 Elpi Accumulate lp:{{
 
+:name "start"
 main [const-decl N (some B) Arity] :- !, std.do! [
   % compute the universe for the structure (default )
   prod-last {coq.arity->term Arity} Ty,
@@ -694,6 +703,7 @@ Elpi Accumulate File "HB/context.elpi".
 Elpi Accumulate File "HB/instance.elpi".
 Elpi Accumulate lp:{{
 
+:name "start"
 main [const-decl Name (some BodySkel) TyWPSkel] :- !,
   with-attributes (with-logging (instance.declare-const Name BodySkel TyWPSkel _)).
 main [T0, F0] :- !,
@@ -727,6 +737,8 @@ Elpi Accumulate File "HB/context.elpi".
 Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate File "HB/factory.elpi".
 Elpi Accumulate lp:{{
+
+:name "start"
 main [A] :- (A = indt-decl _ ; A = const-decl _ _ _), !,
   with-attributes (with-logging (factory.declare A)).
 
@@ -788,9 +800,12 @@ Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate File "HB/factory.elpi".
 Elpi Accumulate File "HB/builders.elpi".
 Elpi Accumulate lp:{{
+
+:name "start"
 main [ctx-decl C] :- !, with-attributes (with-logging (builders.begin C)).
 
 main _ :- coq.error "Usage: HB.builders Context A (f : F1 A).".
+
 }}.
 Elpi Typecheck.
 Elpi Export HB.builders.
@@ -810,8 +825,11 @@ Elpi Accumulate File "HB/context.elpi".
 Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate File "HB/builders.elpi".
 Elpi Accumulate lp:{{
+
+:name "start"
 main [] :- !, with-attributes (with-logging builders.end).
 main _ :- coq.error "Usage: HB.end.".
+
 }}.
 Elpi Typecheck.
 Elpi Export HB.end.
@@ -858,8 +876,11 @@ Elpi Accumulate File "HB/common/utils.elpi".
 Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate lp:{{
+
+:name "start"
 main [str M] :- !, with-attributes (with-logging (export.any M)).
 main _ :- coq.error "Usage: HB.export M.".
+
 }}.
 Elpi Typecheck.
 Elpi Export HB.export.
@@ -884,9 +905,12 @@ Elpi Accumulate File "HB/common/utils.elpi".
 Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate File "HB/export.elpi".
 Elpi Accumulate lp:{{
+
+:name "start"
 main [] :- !, with-attributes (with-logging (export.reexport-all-modules-and-CS none)).
 main [str M] :- !, with-attributes (with-logging (export.reexport-all-modules-and-CS (some M))).
 main _ :- coq.error "Usage: HB.reexport.".
+
 }}.
 Elpi Typecheck.
 Elpi Export HB.reexport.
@@ -930,9 +954,12 @@ Elpi Accumulate File "HB/common/utils.elpi".
 Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate File "HB/lock.elpi".
 Elpi Accumulate lp:{{
+
+:name "start"
 main [const-decl Name (some BoSkel) TySkel] :- !,
   with-attributes (with-logging (lock.lock-def Name TySkel BoSkel)).
 main _ :- coq.error "Usage: HB.lock Definition name : ty := t.".
+
 }}.
 Elpi Typecheck.
 Elpi Export HB.lock.
@@ -985,6 +1012,7 @@ Elpi Accumulate File "HB/context.elpi".
 Elpi Accumulate File "HB/factory.elpi".
 Elpi Accumulate lp:{{
 
+:name "start"
 main [Ctx] :- Ctx = ctx-decl _, !,
   with-attributes (with-logging (
     factory.argument->w-mixins Ctx (pr FLwP _),
@@ -1013,6 +1041,8 @@ Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/utils.elpi".
 Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate lp:{{
+
+:name "start"
 main [trm Skel] :- !, with-attributes (with-logging (check-or-not Skel)).
 main _ :- coq.error "usage: HB.check (term).".