blob: 48b29ea5ed6e05abfb72c893376de3eb10ee23a0 (
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
|
(* $Id$ *)
open Term
open Proof_type
open Tacmach
open Tacentries
let h_clear ids = v_clear [(Clause ids)]
let h_move dep id1 id2 =
(if dep then v_move else v_move_dep) [Identifier id1;Identifier id2]
let h_contradiction = v_contradiction []
let h_reflexivity = v_reflexivity []
let h_symmetry = v_symmetry []
let h_assumption = v_assumption []
let h_absurd c = v_absurd [(Constr c)]
let h_exact c = v_exact [(Constr c)]
let h_one_constructor i = v_constructor [(Integer i)]
let h_any_constructor = v_constructor []
let h_transitivity c = v_transitivity [(Constr c)]
let h_simplest_left = v_left [(Cbindings [])]
let h_simplest_right = v_right [(Cbindings [])]
let h_split c = v_split [(Constr c);(Cbindings [])]
let h_apply c s = v_apply [(Constr c);(Cbindings s)]
let h_simplest_apply c = v_apply [(Constr c);(Cbindings [])]
let h_cut c = v_cut [(Constr c)]
let h_simplest_elim c = v_elim [(Constr c);(Cbindings [])]
let h_elimType c = v_elimType [(Constr c)]
let h_inductionInt i = v_induction[(Integer i)]
let h_inductionId id = v_induction[(Identifier id)]
let h_simplest_case c = v_case [(Constr c);(Cbindings [])]
let h_caseType c = v_caseType [(Constr c)]
let h_destructInt i = v_destruct [(Integer i)]
let h_destructId id = v_destruct [(Identifier id)]
|
