blob: fedea84708c93d8d4f4256012ee31d7cdbc19a9b (
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
|
(*i $Id$ i*)
(*i*)
open Names
open Term
open Sign
open Environ
open Evd
open Proof_type
open Tacmach
open Clenv
(*i*)
(* A somewhat cryptic module. *)
val pf_get_new_id : identifier -> goal sigma -> identifier
val pf_get_new_ids : identifier list -> goal sigma -> identifier list
type arg_binder =
| Dep of identifier
| Nodep of int
| Abs of int
type arg_bindings = (arg_binder * constr) list
type wc = walking_constraints
val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
val add_prod_rel : 'a evar_map -> constr * env -> constr * env
val add_prods_rel : 'a evar_map -> constr * env -> constr * env
(*i**
val add_prod_sign :
'a evar_map -> constr * types signature -> constr * types signature
val add_prods_sign :
'a evar_map -> constr * types signature -> constr * types signature
**i*)
val res_pf_THEN :
(wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic) -> tactic
(* This behaves as [res_pf_THEN] but the tactic applied then takes
also the subgoal number (starting from 1) as argument *)
val res_pf_THEN_i :
(wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
val elim_res_pf_THEN_i :
(wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
val mk_clenv_using : wc -> constr -> wc clausenv
val applyUsing : constr -> tactic
val clenv_apply_n_times : int -> wc clausenv -> wc clausenv
|
