From 9894cffae9662f0473ab3f8696e8ca498cc9cdec Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 21 Jun 2018 17:37:33 +0200
Subject: 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.
---
 test-suite/output/Quote.v | 36 ------------------------------------
 1 file changed, 36 deletions(-)
 delete mode 100644 test-suite/output/Quote.v

(limited to 'test-suite')

diff --git a/test-suite/output/Quote.v b/test-suite/output/Quote.v
deleted file mode 100644
index 2c373d5052..0000000000
--- a/test-suite/output/Quote.v
+++ /dev/null
@@ -1,36 +0,0 @@
-Require Import Quote.
-
-Parameter A B : Prop.
-
-Inductive formula : Type :=
-  | f_and : formula -> formula -> formula
-  | f_or : formula -> formula -> formula
-  | f_not : formula -> formula
-  | f_true : formula
-  | f_atom : index -> formula
-  | f_const : Prop -> formula.
-
-Fixpoint interp_f (vm:
-                    varmap Prop) (f:formula) {struct f} : Prop :=
-  match f with
-  | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
-  | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
-  | f_not f1 => ~ interp_f vm f1
-  | f_true => True
-  | f_atom i => varmap_find True i vm
-  | f_const c => c
-  end.
-
-Goal A \/ B -> A /\ (B \/ A) /\ (A \/ ~ B).
-intro H.
-match goal with
-  | H : ?a \/ ?b |- _ => quote interp_f in a using (fun x => idtac x; change (x \/ b) in H)
-end.
-match goal with
-  |- ?g => quote interp_f [ A ] in g using (fun x => idtac x)
-end.
-quote interp_f.
-Show.
-simpl; quote interp_f [ A ].
-Show.
-Admitted.
-- 
cgit v1.2.3