diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-06 16:59:27 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-17 11:52:38 +0100 |
commit | 653de32139ecee3114779a5ee2961c58793889e5 (patch) | |
tree | 5afe95bfaa5af025f92e9aea27147862487c0fb0 /plugins/ltac/tacintern.mli | |
parent | bcb634d070519d6e37d9b7d39f12437a7d38f0c2 (diff) |
Ltac as a plugin.
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
Diffstat (limited to 'plugins/ltac/tacintern.mli')
-rw-r--r-- | plugins/ltac/tacintern.mli | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli new file mode 100644 index 000000000..71ca354fa --- /dev/null +++ b/plugins/ltac/tacintern.mli @@ -0,0 +1,64 @@ +(************************************************************************) +(* 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 Pp +open Names +open Tacexpr +open Genarg +open Constrexpr +open Misctypes + +(** Globalization of tactic expressions : + Conversion from [raw_tactic_expr] to [glob_tactic_expr] *) + +type glob_sign = Genintern.glob_sign = { + ltacvars : Id.Set.t; + genv : Environ.env } + +val fully_empty_glob_sign : glob_sign + +val make_empty_glob_sign : unit -> glob_sign + (** same as [fully_empty_glob_sign], but with [Global.env()] as + environment *) + +(** Main globalization functions *) + +val glob_tactic : raw_tactic_expr -> glob_tactic_expr + +val glob_tactic_env : + Id.t list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr + +(** Low-level variants *) + +val intern_pure_tactic : glob_sign -> raw_tactic_expr -> glob_tactic_expr + +val intern_tactic_or_tacarg : + glob_sign -> raw_tactic_expr -> Tacexpr.glob_tactic_expr + +val intern_constr : glob_sign -> constr_expr -> glob_constr_and_expr + +val intern_constr_with_bindings : + glob_sign -> constr_expr * constr_expr bindings -> + glob_constr_and_expr * glob_constr_and_expr bindings + +val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located + +(** Adds a globalization function for extra generic arguments *) + +val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument + +(** printing *) +val print_ltac : Libnames.qualid -> std_ppcmds + +(** Reduction expressions *) + +val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr +val dump_glob_red_expr : raw_red_expr -> unit + +(* Hooks *) +val strict_check : bool ref |