Refactor import for Coq_Dep

Author: FissoreD

apps/tc/theories/add_commands.v

@@ -3,6 +3,7 @@
 
 From elpi.apps Require Import db.
 
+From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc Extra Dependency "solver.elpi" as solver.
@@ -57,8 +58,8 @@ Elpi Typecheck.
 Elpi Command TC.AddHook.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
-  accumulate elpi/tc_aux.
   pred addHook i:grafting, i:string. 
   addHook Grafting NewName :- 
     @global! => add-tc-db NewName Grafting (hook NewName).

apps/tc/theories/db.v

@@ -3,6 +3,9 @@
 
 From elpi Require Import elpi.
 
+From elpi.apps.tc Extra Dependency "base.elpi".
+From elpi.apps.tc Extra Dependency "tc_aux.elpi".
+
 (* 
   tc_option.db contains the set of options used by the solver of tc. 
   all the options are set to false by default

apps/tc/theories/tc.v

@@ -3,6 +3,7 @@
 
 Declare ML Module "coq-elpi-tc.plugin".
 
+From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
@@ -81,8 +82,8 @@ Elpi Typecheck.
 Elpi Command TC.Set_deterministic.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
-  accumulate elpi/tc_aux.
   main [str ClassStr] :- 
     coq.locate ClassStr ClassGR, 
     std.assert! (coq.TC.class? ClassGR) "Should pass the name of a type class",