remove addmode flag (now is always on)

LPCIC · Nov 7, 2023 · d2c2955 · d2c2955
1 parent 7970f55
commit d2c2955
Show file tree

Hide file tree

Showing 5 changed files with 2 additions and 8 deletions.
diff --git a/apps/tc/README.md b/apps/tc/README.md
@@ -551,8 +551,7 @@ Here the list of the flags available (all of them are `off` by default):
 ## WIP
 
 1. Mode management: 
-   - Classes with multiple modes ??
+   - Classes with multiple modes 
 2. Clarify pattern fragment unification 
 3. Topological sort of premises in modes are activated 
-4. Option to disable auto compiler (maybe)
 
diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi
@@ -17,7 +17,6 @@ coq-mode->elpi mode-output (pr out "term").
 
 pred modes-of-class i:gref, o:list (pair argument_mode string).
 modes-of-class ClassGr Modes :- 
-  is-option-active {oTC-addModes},
   coq.hints.modes ClassGr "typeclass_instances" CoqModesList,
   not (CoqModesList = []),
   std.assert! (CoqModesList = [HintModesFst]) "At the moment we only allow TC with one Hint Mode",

diff --git a/apps/tc/tests/classes_declare.v b/apps/tc/tests/classes_declare.v
@@ -47,7 +47,6 @@ End S2.
 
 (* Mode test *)
 Section S3.
-  Set TC AddModes.
   #[mode(i)] TC.Declare Class class3 (n : nat).
   Instance inst3 : class3 0. Proof. apply Build_class3. Qed.
 

diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
@@ -22,9 +22,6 @@ Elpi Db tc_options.db lp:{{
 
   pred oTC-debug o:list string.
   oTC-debug ["TC", "Debug"].
-
-  pred oTC-addModes o:list string.
-  oTC-addModes ["TC", "AddModes"].
 
   pred oTC-use-pattern-fragment-compiler o:list string. 
   oTC-use-pattern-fragment-compiler ["TC", "CompilerWithPatternFragment"].

diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
@@ -46,7 +46,7 @@ Elpi Accumulate File solver.
 Elpi Query lp:{{
   sigma Options\ 
     Options = [oTC-ignore-eta-reduction, oTC-resolution-time, 
-      oTC-clauseNameShortName, oTC-time-refine, oTC-debug, oTC-addModes,
+      oTC-clauseNameShortName, oTC-time-refine, oTC-debug, 
       oTC-use-pattern-fragment-compiler],
     std.forall Options (x\ sigma Args\ x Args, 
       coq.option.add Args (coq.option.bool ff) ff).