blob: d37582bd7901bf7fef083d11d81d1f505d648170 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
(************************************************************************)
(* 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 Term
open Libnames
open Constrexpr
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 }
|
