blob: fc72bd4e4686ae6d839b7dbe7265af510eab2ba8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
open Pp
open Names
open Term
open Glob_term
open Proof_type
open Constrexpr
open Misctypes
val lemInv_gen : quantified_hypothesis -> constr -> tactic
val lemInvIn_gen : quantified_hypothesis -> constr -> identifier list -> tactic
val lemInv_clause :
quantified_hypothesis -> constr -> identifier list -> tactic
val inversion_lemma_from_goal :
int -> identifier -> identifier located -> sorts -> bool ->
(identifier -> tactic) -> unit
val add_inversion_lemma_exn :
identifier -> constr_expr -> glob_sort -> bool -> (identifier -> tactic) ->
unit
|