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. --- theories/Sorting/PermutEq.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Sorting') diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v index 995a77cce..87ffce0b6 100644 --- a/theories/Sorting/PermutEq.v +++ b/theories/Sorting/PermutEq.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation. +Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Omega. Set Implicit Arguments. -- cgit v1.2.3