blob: 0366cd25b21fe40537c99c79541206f8b0ade146 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* $Id$ *)
(*i*)
open Pp
open Proof_trees
(*i*)
val pr_prim_rule : prim_rule -> std_ppcmds
val prim_refiner : prim_rule -> 'a Evd.evar_map -> goal -> goal list
val prim_extractor :
((type_judgement, constr) env -> proof_tree -> constr) ->
(type_judgement, constr) env -> proof_tree -> constr
val extract_constr : constr assumptions -> constr -> constr
|
