base file loaded once

Author: FissoreD

apps/tc/tests/importOrder/sameOrderCommand.v

@@ -1,6 +1,5 @@
 From elpi.apps Require Export tc.
 
-From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
 From elpi.apps.tc.elpi Extra Dependency "tc_same_order.elpi" as tc_same_order.
@@ -11,7 +10,6 @@ Set Warnings "+elpi".
 Elpi Command SameOrderImport.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif.
 Elpi Accumulate File compile_goal.

apps/tc/theories/add_commands.v

@@ -10,7 +10,6 @@ From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
-From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc.elpi Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
@@ -20,7 +19,7 @@ Set Warnings "+elpi".
 Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate File unif modes link.
 Elpi Accumulate lp:{{  
@@ -33,7 +32,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate File unif modes link.
 Elpi Accumulate File parser_addInstances.
@@ -46,7 +45,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddAllClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux modes.
+Elpi Accumulate File tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   % Ignore is the list of classes we do not want to add
@@ -59,7 +58,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux modes.
+Elpi Accumulate File tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   pred tc.add-all-classes i:list argument , i:tc.search-mode.
@@ -77,7 +76,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddHook.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
   pred tc.addHook i:grafting, i:string. 
   tc.addHook Grafting NewName :- 
@@ -107,7 +106,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Declare.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux modes.
+Elpi Accumulate File tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main _ :- coq.warning "TC.Declare" {tc.warning-name} 
@@ -121,7 +120,7 @@ with implicit arguments (those implicits will be neglected)", fail.
 Elpi Command TC.Pending_mode.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux modes.
+Elpi Accumulate File tc_aux modes.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main M :- 
@@ -134,7 +133,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.AddRecordFields.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate  lp:{{
   pred tc.add_tc.records_unif.aux i:int, i:term, i:list term, i:constant, o:prop.
   tc.add_tc.records_unif.aux 0 T Args ProjConstant P :- !,

apps/tc/theories/tc.v

@@ -9,7 +9,6 @@ From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 
 From elpi.apps.tc.elpi Extra Dependency "link.elpi" as link.
-From elpi.apps.tc.elpi Extra Dependency "base.elpi" as base.
 From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc.elpi Extra Dependency "compile_goal.elpi" as compile_goal.
 From elpi.apps.tc.elpi Extra Dependency "compile_instance.elpi" as compile_instance.
@@ -50,7 +49,7 @@ Elpi Accumulate lp:{{
 Elpi Tactic TC.Solver.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif modes link.
 Elpi Accumulate File compile_instance compile_goal.
 Elpi Accumulate File solver.
@@ -75,7 +74,7 @@ Elpi Query lp:{{
 Elpi Command TC.Compiler.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File unif modes link.
 Elpi Accumulate File compile_instance compiler compile_goal.
 Elpi Accumulate File create_tc_predicate.
@@ -123,7 +122,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Set_deterministic.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
   main [str ClassStr] :- 
     coq.locate ClassStr ClassGR, 
@@ -137,7 +136,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Get_class_info.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
   main [str ClassStr] :- 
     coq.locate ClassStr ClassGR, 
@@ -157,7 +156,7 @@ Elpi Accumulate lp:{{
 Elpi Command TC.Unfold.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate Db tc.db.
-Elpi Accumulate File base tc_aux.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
   pred tc.add-unfold i:gref.
   tc.add-unfold (const C) :-