Skip to content

Commit 6fc045d

Browse files
authored
Merge pull request #1207 from SkySkimmer/no-auto-scheme
Adapt to rocq-prover/rocq#21245 (no autogenerated eq_rew schemes)
2 parents 722ba95 + 5698fae commit 6fc045d

File tree

2 files changed

+1
-4
lines changed

2 files changed

+1
-4
lines changed

template-rocq/_PluginProject.in

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -80,8 +80,6 @@ gen-src/eqDec.ml
8080
gen-src/eqDec.mli
8181
gen-src/eqDecInstances.ml
8282
gen-src/eqDecInstances.mli
83-
gen-src/eqdepFacts.ml
84-
gen-src/eqdepFacts.mli
8583
gen-src/equalities.ml
8684
gen-src/equalities.mli
8785
gen-src/extractable.ml

template-rocq/gen-src/metarocq_template_plugin.mlpack

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,6 @@ Logic1
5959
Logic2
6060
Number
6161
Relation
62-
EqdepFacts
6362
MRPrelude
6463
MRReflect
6564
ReflectEq
@@ -87,6 +86,7 @@ Sint63
8786
Show
8887
MRUtils
8988
Signature
89+
Logic0
9090
All_Forall
9191
MRFSets
9292
MRMSets
@@ -106,7 +106,6 @@ Reflect
106106
Pretty
107107
Common0
108108
Extractable
109-
Logic0
110109
EnvMap
111110

112111
Tm_util

0 commit comments

Comments
 (0)