From 4a0e4ee76663a12e3cb3d22ce77b0d37a5830af5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 16 Feb 2014 00:30:20 +0100 Subject: Now parsing rules of ML-declared tactics are only made available after the corresponding Declare ML Module command. This changes essentially two things: 1. ML plugins are forced to use the DECLARE PLUGIN statement before any TACTIC EXTEND statement. The plugin name must be exactly the string passed to the Declare ML Module command. 2. ML tactics are only made available after the Coq module that does the corresponding Declare ML Module is imported. This may break a few things, as it already broke quite some uses of omega in the stdlib. --- plugins/btauto/Algebra.v | 2 +- plugins/btauto/Reflect.v | 2 +- plugins/btauto/g_btauto.ml4 | 2 ++ plugins/cc/g_congruence.ml4 | 2 ++ plugins/firstorder/g_ground.ml4 | 2 ++ plugins/fourier/g_fourier.ml4 | 2 ++ plugins/funind/g_indfun.ml4 | 2 ++ plugins/micromega/g_micromega.ml4 | 2 ++ plugins/nsatz/nsatz.ml4 | 2 ++ plugins/omega/g_omega.ml4 | 2 ++ plugins/quote/g_quote.ml4 | 2 ++ plugins/romega/g_romega.ml4 | 2 ++ plugins/rtauto/g_rtauto.ml4 | 2 ++ plugins/setoid_ring/Rings_Z.v | 1 + plugins/setoid_ring/newring.ml4 | 2 ++ 15 files changed, 27 insertions(+), 2 deletions(-) (limited to 'plugins') diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index 795211c20..bc5a39002 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -1,4 +1,4 @@ -Require Import Bool PArith DecidableClass ROmega. +Require Import Bool PArith DecidableClass Omega ROmega. Ltac bool := repeat match goal with diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index e31948ffe..8a95d5b4b 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -1,4 +1,4 @@ -Require Import Bool DecidableClass Algebra Ring PArith ROmega. +Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega. Section Bool. diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 index a45203d3d..ce99756e0 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "btauto_plugin" + TACTIC EXTEND btauto | [ "btauto" ] -> [ Refl_btauto.Btauto.tac ] END diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index c2c437c80..5d6f172c4 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -10,6 +10,8 @@ open Cctac +DECLARE PLUGIN "cc_plugin" + (* Tactic registration *) TACTIC EXTEND cc diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 9ae8fcbf6..c3ae05de6 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -16,6 +16,8 @@ open Tacticals open Tacinterp open Libnames +DECLARE PLUGIN "ground_plugin" + (* declaring search depth as a global option *) let ground_depth=ref 3 diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index 1635cecc0..11107385d 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -10,6 +10,8 @@ open FourierR +DECLARE PLUGIN "fourier_plugin" + TACTIC EXTEND fourier [ "fourierz" ] -> [ Proofview.V82.tactic fourier ] END diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 90282fcf7..21d0b9f3d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -19,6 +19,8 @@ open Genarg open Tacticals open Misctypes +DECLARE PLUGIN "recdef_plugin" + let pr_binding prc = function | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 78d1e1756..7ed40acb4 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -19,6 +19,8 @@ open Errors open Misctypes +DECLARE PLUGIN "micromega_plugin" + let out_arg = function | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") | ArgArg x -> x diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 6fd8ab8e9..20b3ac1e1 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -17,6 +17,8 @@ open Coqlib open Num open Utile +DECLARE PLUGIN "nsatz_plugin" + (*********************************************************************** Operations on coefficients *) diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index b384478ae..83092ccc4 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -15,6 +15,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "omega_plugin" + open Coq_omega let omega_tactic l = diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 1f11b07ad..47a62c9e6 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -14,6 +14,8 @@ open Tacexpr open Geninterp open Quote +DECLARE PLUGIN "quote_plugin" + let loc = Loc.ghost let cont = (loc, Id.of_string "cont") let x = (loc, Id.of_string "x") diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index c07825f8c..4b6c9b790 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "romega_plugin" + open Refl_omega let romega_tactic l = diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index 7d0b7a1bc..b90854701 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "rtauto_plugin" + TACTIC EXTEND rtauto [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ] END diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v index 58a4d7ea6..605a23a98 100644 --- a/plugins/setoid_ring/Rings_Z.v +++ b/plugins/setoid_ring/Rings_Z.v @@ -1,6 +1,7 @@ Require Export Cring. Require Export Integral_domain. Require Export Ncring_initial. +Require Export Omega. Instance Zcri: (Cring (Rr:=Zr)). red. exact Z.mul_comm. Defined. diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 8df061870..8d83ffc33 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -31,6 +31,8 @@ open Decl_kinds open Entries open Misctypes +DECLARE PLUGIN "newring_plugin" + (****************************************************************************) (* controlled reduction *) -- cgit v1.2.3