diff options
| author | Emilio Jesus Gallego Arias | 2020-03-07 01:04:46 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 06:02:07 -0400 |
| commit | 4f81cc44e5af01f40ad972a7285edd2c40c178c7 (patch) | |
| tree | d8680af1f1eb5adfeada874613a1c5fc61c31073 /tactics | |
| parent | bc70bb31c579b9482d0189f20806632c62b26a61 (diff) | |
[proof] Start of mutual definition save refactoring.
First commit of a series that will unify (and enforce) the handling of
mutual constants. We will split this in several commits as to easy
debugging / bisect in case of problems.
In this first commit, we move the actual declare logic to a common
place.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/proof_global.ml | 8 | ||||
| -rw-r--r-- | tactics/proof_global.mli | 4 |
2 files changed, 1 insertions, 11 deletions
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index 7fd1634dcf..623e6b8a42 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -8,14 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(***********************************************************************) -(* *) -(* This module defines proof facilities relevant to the *) -(* toplevel. In particular it defines the global proof *) -(* environment. *) -(* *) -(***********************************************************************) - open Util open Names open Context diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index f1281d1291..e1c75c0649 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -8,9 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** This module defines proof facilities relevant to the - toplevel. In particular it defines the global proof - environment. *) +(** State for interactive proofs. *) type t |