blob: 3bcf1af0e246f11541b0f790f08da24e38708476 (
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
(***********************************************************************)
(* 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
val qflag : bool ref
val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) ->
'a -> 'a -> 'b -> 'b -> int
val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) ->
'a -> 'a -> 'b -> 'b -> 'c ->'c -> int
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 list
|Forall of constr*constr
|Atom of constr
|Evaluable of Names.evaluable_global_reference * Term.constr
|False
type counter = bool -> metavariable
val construct_nhyps : inductive -> int array
val ind_hyps : int -> inductive -> constr list -> Sign.rel_context array
val kind_of_formula : constr -> kind_of_formula
val build_atoms : Proof_type.goal Tacmach.sigma -> counter ->
bool -> constr -> (bool*constr) list
type right_pattern =
Rand
| Ror
| Rforall
| Rexists of metavariable*constr
| Rarrow
| Revaluable of Names.evaluable_global_reference
type right_formula =
Complex of right_pattern*constr*((bool*constr) list)
| Atomic of constr
type left_arrow_pattern=
LLatom
| LLfalse
| LLand of inductive*constr list
| LLor of inductive*constr list
| LLforall of constr
| LLexists of inductive*constr list
| LLarrow of constr*constr*constr
| LLevaluable of Names.evaluable_global_reference
type left_pattern=
Lfalse
| Land of inductive
| Lor of inductive
| Lforall of metavariable*constr
| Lexists
| Levaluable of Names.evaluable_global_reference
| LA of constr*left_arrow_pattern
type left_formula={id:global_reference;
constr:constr;
pat:left_pattern;
atoms:(bool*constr) list;
internal:bool}
exception Is_atom of constr
val build_left_entry :
global_reference -> types -> bool -> Proof_type.goal Tacmach.sigma ->
counter -> (left_formula,types) sum
val build_right_entry : types -> Proof_type.goal Tacmach.sigma ->
counter -> right_formula
|
