blob: dfc90a1bf7d7bccf41c0295d43deaa450e7baa33 (
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
64
65
66
67
68
69
70
71
72
73
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Term
open Names
open Libnames
type ('a,'b) sum = Left of 'a | Right of 'b
type kind_of_formula=
Arrow of constr*constr
|And of inductive*constr list
|Or of inductive*constr list
|Exists of inductive*constr*constr*constr
|Forall of constr*constr
|Atom of constr
|False
type counter = bool -> int
val newcnt : unit -> counter
val construct_nhyps : inductive -> int array
exception Dependent_Inductive
val ind_hyps : inductive -> constr list -> Sign.rel_context array
val kind_of_formula : constr -> kind_of_formula
type right_pattern =
Rand
| Ror
| Rforall
| Rexists of int*constr
| Rarrow
type right_formula =
Complex of right_pattern*((bool*constr) list)
| Atomic of constr
type left_pattern=
Lfalse
| Land of inductive
| Lor of inductive
| Lforall of int*constr
| Lexists
| LAatom of constr
| LAfalse
| LAand of inductive*constr list
| LAor of inductive*constr list
| LAforall of constr
| LAexists of inductive*constr*constr*constr
| LAarrow of constr*constr*constr
type left_formula={id:global_reference;
pat:left_pattern;
atoms:(bool*constr) list;
internal:bool}
val build_left_entry :
global_reference -> types -> bool -> counter -> (left_formula,types) sum
val build_right_entry : types -> counter -> right_formula
|
