blob: dd3630a0df0fa824cb2320ad732da5f43e43b7ba (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
val generate_new_structural_principle :
(* induction principle on rel *)
Names.constant ->
(* the elimination sort *)
Term.sorts ->
(* Name of the new principle *)
(Names.identifier) option ->
(* do we want to use a principle with conclusion *)
bool ->
(* the compute functions to use *)
Names.constant array ->
int ->
unit
val my_reflexivity : Tacmach.tactic
|
