diff options
Diffstat (limited to 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 6dcafb77a..56f5facf8 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -10,6 +10,7 @@ open Evd open Proof_type +open EConstr (** The refiner (handles primitive rules and high-level tactics). *) @@ -17,7 +18,7 @@ val sig_it : 'a sigma -> 'a val project : 'a sigma -> evar_map val pf_env : goal sigma -> Environ.env -val pf_hyps : goal sigma -> Context.Named.t +val pf_hyps : goal sigma -> named_context val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma |