diff options
| author | Maxime Dénès | 2018-03-10 12:40:04 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-10 12:40:04 +0100 |
| commit | 33c5d8d00cb017c61141ee0d6b7cb8f672a3e691 (patch) | |
| tree | c7185ce535ef7c5438e79f1c4b81464c8367d6c9 /plugins/setoid_ring | |
| parent | 4d5c7243b4aea5b28358757e2d86c11334da6699 (diff) | |
| parent | 99129d2518bd9fe92051aa89138cbb57c839a270 (diff) | |
Merge PR #6869: [ssreflect] Fix module scoping problems due to packing and mli files.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring_ast.ml | 67 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring_ast.mli | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring_plugin.mlpack | 1 |
3 files changed, 70 insertions, 0 deletions
diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml new file mode 100644 index 0000000000..3eb68b5189 --- /dev/null +++ b/plugins/setoid_ring/newring_ast.ml @@ -0,0 +1,67 @@ +(************************************************************************) +(* * 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 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Constr +open Libnames +open Constrexpr + +open Ltac_plugin +open Tacexpr + +type 'constr coeff_spec = + Computational of 'constr (* equality test *) + | Abstract (* coeffs = Z *) + | Morphism of 'constr (* general morphism *) + +type cst_tac_spec = + CstTac of raw_tactic_expr + | Closed of reference list + +type 'constr ring_mod = + Ring_kind of 'constr coeff_spec + | Const_tac of cst_tac_spec + | Pre_tac of raw_tactic_expr + | Post_tac of raw_tactic_expr + | Setoid of constr_expr * constr_expr + | Pow_spec of cst_tac_spec * constr_expr + (* Syntaxification tactic , correctness lemma *) + | Sign_spec of constr_expr + | Div_spec of constr_expr + +type 'constr field_mod = + Ring_mod of 'constr ring_mod + | Inject of constr_expr + +type ring_info = + { ring_carrier : types; + ring_req : constr; + ring_setoid : constr; + ring_ext : constr; + ring_morph : constr; + ring_th : constr; + ring_cst_tac : glob_tactic_expr; + ring_pow_tac : glob_tactic_expr; + ring_lemma1 : constr; + ring_lemma2 : constr; + ring_pre_tac : glob_tactic_expr; + ring_post_tac : glob_tactic_expr } + +type field_info = + { field_carrier : types; + field_req : constr; + field_cst_tac : glob_tactic_expr; + field_pow_tac : glob_tactic_expr; + field_ok : constr; + field_simpl_eq_ok : constr; + field_simpl_ok : constr; + field_simpl_eq_in_ok : constr; + field_cond : constr; + field_pre_tac : glob_tactic_expr; + field_post_tac : glob_tactic_expr } diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index 226c65125e..3eb68b5189 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -11,6 +11,8 @@ open Constr open Libnames open Constrexpr + +open Ltac_plugin open Tacexpr type 'constr coeff_spec = diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack index 23663b4090..5aa79b5868 100644 --- a/plugins/setoid_ring/newring_plugin.mlpack +++ b/plugins/setoid_ring/newring_plugin.mlpack @@ -1,2 +1,3 @@ +Newring_ast Newring G_newring |