diff options
| author | Pierre Letouzey | 2016-06-23 15:07:02 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2017-06-14 12:02:35 +0200 |
| commit | 27c8e30fad95d887b698b0e3fa563644c293b033 (patch) | |
| tree | 021febbccb12aff7873cf18aebaf4e9e2a6e4d47 /plugins/funind | |
| parent | b240771a3661883ca0cc0497efee5b48519bddea (diff) | |
Prelude : no more autoload of plugins extraction and recdef
The user now has to manually load them, respectively via:
Require Extraction
Require Import FunInd
The "Import" in the case of FunInd is to ensure that the
tactics functional induction and functional inversion are indeed
in scope.
Note that the Recdef.v file is still there as well (it contains
complements used when doing Function with measures), and it also
triggers a load of FunInd.v.
This change is correctly documented in the refman, and the test-suite
has been adapted.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/FunInd.v | 10 | ||||
| -rw-r--r-- | plugins/funind/Recdef.v | 2 |
2 files changed, 11 insertions, 1 deletions
diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v new file mode 100644 index 0000000000..e40aea7764 --- /dev/null +++ b/plugins/funind/FunInd.v @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Coq.extraction.Extraction. +Declare ML Module "recdef_plugin". diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v index e4433247b4..c6fcd647ff 100644 --- a/plugins/funind/Recdef.v +++ b/plugins/funind/Recdef.v @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Import Coq.funind.FunInd. Require Import PeanoNat. - Require Compare_dec. Require Wf_nat. |