blob: cbab2a90caac009558d9391c28cf3dfec4bc54e6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* $Id$ *)
(*i*)
open Term
open Sign
open Evd
open Environ
open Proof_trees
(*i*)
val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list
val prim_extractor :
((typed_type, constr) env -> proof_tree -> constr) ->
(typed_type, constr) env -> proof_tree -> constr
val extract_constr : constr assumptions -> constr -> constr
|
