diff options
Diffstat (limited to 'plugins/setoid_ring/newring.mli')
| -rw-r--r-- | plugins/setoid_ring/newring.mli | 56 |
1 files changed, 12 insertions, 44 deletions
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index f417c87c..1d1557b1 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -1,46 +1,30 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names -open Constr +open EConstr open Libnames open Globnames open Constrexpr -open Tacexpr -open Proof_type open Newring_ast val protect_tac_in : string -> Id.t -> unit Proofview.tactic val protect_tac : string -> unit Proofview.tactic -val closed_term : constr -> global_reference list -> unit Proofview.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 closed_term : EConstr.constr -> global_reference list -> unit Proofview.tactic 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 + constr_expr -> + constr_expr ring_mod list -> unit val from_name : ring_info Spmap.t ref @@ -49,26 +33,10 @@ val ring_lookup : 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 + constr_expr -> + constr_expr field_mod list -> unit val field_from_name : field_info Spmap.t ref |