diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-25 13:40:13 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-25 14:41:09 +0100 |
commit | 4e515c483e41f0362bf1102f8e8ae071fdcf04f7 (patch) | |
tree | fba76ab0d5a3b5b1cf55b35e6c58e102b7fb6d7c /plugins/setoid_ring/newring.mli | |
parent | 43c6f29edde078726f10144c0d241a882ebdd13d (diff) |
Adding a proper interface to Newring.
The ring ASTs were put in a separate interface, and only the
extension-related code was put in a dedicated G_newring file.
Diffstat (limited to 'plugins/setoid_ring/newring.mli')
-rw-r--r-- | plugins/setoid_ring/newring.mli | 78 |
1 files changed, 78 insertions, 0 deletions
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli new file mode 100644 index 000000000..4bd3383d6 --- /dev/null +++ b/plugins/setoid_ring/newring.mli @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Constr +open Libnames +open Globnames +open Constrexpr +open Tacexpr +open Proof_type +open Newring_ast + +val protect_tac_in : string -> Id.t -> tactic + +val protect_tac : string -> tactic + +val closed_term : constr -> global_reference list -> tactic + +val process_ring_mods : + constr_expr ring_mod list -> + constr coeff_spec * (constr * constr) option * + cst_tac_spec option * raw_tactic_expr option * + raw_tactic_expr option * + (cst_tac_spec * constr_expr) option * + constr_expr option * constr_expr option + +val add_theory : + Id.t -> + Evd.evar_map * constr -> + (constr * constr) option -> + constr coeff_spec -> + cst_tac_spec option -> + raw_tactic_expr option * raw_tactic_expr option -> + (cst_tac_spec * constr_expr) option -> + constr_expr option -> + constr_expr option -> unit + +val ic : constr_expr -> Evd.evar_map * constr + +val from_name : ring_info Spmap.t ref + +val ring_lookup : + glob_tactic_expr -> + constr list -> + constr list -> constr -> unit Proofview.tactic + +val process_field_mods : + constr_expr field_mod list -> + constr coeff_spec * + (constr * constr) option * constr option * + cst_tac_spec option * raw_tactic_expr option * + raw_tactic_expr option * + (cst_tac_spec * constr_expr) option * + constr_expr option * constr_expr option + +val add_field_theory : + Id.t -> + Evd.evar_map * constr -> + (constr * constr) option -> + constr coeff_spec -> + cst_tac_spec option -> + constr option -> + raw_tactic_expr option * raw_tactic_expr option -> + (cst_tac_spec * constr_expr) option -> + constr_expr option -> + constr_expr option -> unit + +val field_from_name : field_info Spmap.t ref + +val field_lookup : + glob_tactic_expr -> + constr list -> + constr list -> constr -> unit Proofview.tactic |