diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-27 16:12:58 +0200 |
|---|---|---|
| committer |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-10 23:50:25 +0200 |
| commit | 7f1635816588ae200c8eed381d726bd29f57d899 (patch) | |
| tree | 305b8576ee8387385b80ef4ca07491739490aa38 /vernac/proof_using.mli | |
| parent | ffc91e6fcc7a1f3d719b7ad95dbbd3293e26c653 (diff) | |
[vernac] Remove "Proof using" hacks from parser.
We place `Proof_using` in the proper place [`vernac`] and we remove
gross parsing hacks.
The new placement should allow to use the printers and more convenient
structure, and reduce strange coupling between parsing and internal
representation.
Diffstat (limited to 'vernac/proof_using.mli')
| -rw-r--r-- | vernac/proof_using.mli | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli new file mode 100644 index 000000000..ddab2742d --- /dev/null +++ b/vernac/proof_using.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Utility code for section variables handling in Proof using... *) + +val process_expr : + Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list -> + Names.Id.t list + +val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit + +val to_string : Vernacexpr.section_subset_expr -> string + +val suggest_constant : Environ.env -> Names.Constant.t -> unit + +val suggest_variable : Environ.env -> Names.Id.t -> unit + +val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option |