diff options
Diffstat (limited to 'proofs/logic.mli')
| -rw-r--r-- | proofs/logic.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/logic.mli b/proofs/logic.mli index 27a50af85b..cc9f108ee8 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -4,11 +4,12 @@ (*i*) open Term open Sign +open Evd open Environ open Proof_trees (*i*) -val prim_refiner : prim_rule -> unsafe_env -> goal -> goal list +val prim_refiner : prim_rule -> unsafe_env -> 'a evar_map -> goal -> goal list val prim_extractor : ((typed_type, constr) env -> proof_tree -> constr) -> |