blob: bc07c9a4d6ea4bd8c9d2e2fb96ccf1abc038680b (
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
|
(***********************************************************************)
(* 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 Proof_type
open Tacmach
open Tacentries
let h_clear ids = v_clear [(Clause (List.map (fun x -> InHyp x) 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)]
|
