diff options
| author | Hugo Herbelin | 2020-04-05 14:13:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-21 19:33:19 +0200 |
| commit | c6815a6cd004a1ab4852414127fef6f8f77894bb (patch) | |
| tree | 35e27c74f403844f4fa0408c42109ab20c94cfad /theories/Init | |
| parent | dcced70a3ac146efb2f6214e197ef4b0d73debb1 (diff) | |
Adding a Declare ML Module in empty file Ltac.v.
Indeed, it would be intuitive that `Require Import Ltac` is an
equivalent for Ltac of `Require Import Ltac2.Ltac2`.
Also declaring the classic proof mode.
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Ltac.v | 13 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 4 |
2 files changed, 14 insertions, 3 deletions
diff --git a/theories/Init/Ltac.v b/theories/Init/Ltac.v new file mode 100644 index 0000000000..ac5a69a38a --- /dev/null +++ b/theories/Init/Ltac.v @@ -0,0 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Declare ML Module "ltac_plugin". + +Export Set Default Proof Mode "Classic". diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index a5e4178b93..833fb7464e 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -132,6 +132,4 @@ Open Scope type_scope. (** ML Tactic Notations *) -Declare ML Module "ltac_plugin". - -Global Set Default Proof Mode "Classic". +Require Export Ltac. |