diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-12-18 18:14:58 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-15 20:45:28 +0100 |
| commit | fa9df2efe5666789bf91bb7761567cd53e6c451f (patch) | |
| tree | dfabeded9b4060114e0f9d7f4d3760efc982ae0c /vernac/auto_ind_decl.mli | |
| parent | 0df095ec0715f548180bbff70a6feb673c6726a6 (diff) | |
[stm] Break stm/toplevel dependency loop.
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
Diffstat (limited to 'vernac/auto_ind_decl.mli')
| -rw-r--r-- | vernac/auto_ind_decl.mli | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/vernac/auto_ind_decl.mli b/vernac/auto_ind_decl.mli new file mode 100644 index 000000000..60232ba8f --- /dev/null +++ b/vernac/auto_ind_decl.mli @@ -0,0 +1,42 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +open Names +open Ind_tables + +(** This file is about the automatic generation of schemes about + decidable equality, + @author Vincent Siles + Oct 2007 *) + +(** {6 Build boolean equality of a block of mutual inductive types } *) + +exception EqNotFound of inductive * inductive +exception EqUnknown of string +exception UndefinedCst of string +exception InductiveWithProduct +exception InductiveWithSort +exception ParameterWithoutEquality of Globnames.global_reference +exception NonSingletonProp of inductive +exception DecidabilityMutualNotSupported +exception NoDecidabilityCoInductive + +val beq_scheme_kind : mutual scheme_kind +val build_beq_scheme : mutual_scheme_object_function + +(** {6 Build equivalence between boolean equality and Leibniz equality } *) + +val lb_scheme_kind : mutual scheme_kind +val make_lb_scheme : mutual_scheme_object_function +val bl_scheme_kind : mutual scheme_kind +val make_bl_scheme : mutual_scheme_object_function + +(** {6 Build decidability of equality } *) + +val eq_dec_scheme_kind : mutual scheme_kind +val make_eq_decidability : mutual_scheme_object_function |