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 /test-suite | |
| 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 'test-suite')
| -rw-r--r-- | test-suite/output/Quote.v | 36 |
1 files changed, 0 insertions, 36 deletions
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. |