diff options
| author | Maxime Dénès | 2018-06-21 17:37:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-12 17:04:42 +0200 |
| commit | 9894cffae9662f0473ab3f8696e8ca498cc9cdec (patch) | |
| tree | cf4f5c2366e4a74faa24c33317b2ac802ffc195c /plugins/setoid_ring | |
| parent | e3e1f56c38f345bccf984dd6d6d86fa06e423b96 (diff) | |
Remove quote plugin
As far as I know, this plugin is untested and barely maintained. I don't
think it has real use cases any more, so let's move it out from the repo
and see if somebody wants to take over and maintain it.
We also remove the documentation, which was telling our users to look at
ring to see an example of reification done using quote, when in fact it
wasn't using it anymore.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/Ring_base.v | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v index a9b4d9d6f4..920b13ef49 100644 --- a/plugins/setoid_ring/Ring_base.v +++ b/plugins/setoid_ring/Ring_base.v @@ -12,7 +12,6 @@ ring tactic. Abstract rings need more theory, depending on ZArith_base. *) -Require Import Quote. Declare ML Module "newring_plugin". Require Export Ring_theory. Require Export Ring_tac. diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index e8efb362e2..26fef99bb2 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -15,7 +15,6 @@ Require Import Ring_polynom. Require Import BinList. Require Export ListTactics. Require Import InitialRing. -Require Import Quote. Declare ML Module "newring_plugin". |