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/logic.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/logic.mli') diff --git a/proofs/logic.mli b/proofs/logic.mli index 5fe28ac76..f98248e4d 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -55,7 +55,7 @@ exception RefinerError of refiner_error val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> - Context.Named.Declaration.t -> Environ.named_context_val + EConstr.named_declaration -> Environ.named_context_val val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> Environ.named_context_val -> Environ.named_context_val -- cgit v1.2.3