From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- proofs/refiner.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'proofs/refiner.mli') 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 -- cgit v1.2.3