From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/goal.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs/goal.ml')

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 410e738de..9046f4534 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -155,6 +155,7 @@ module V82 = struct
       with Not_found -> true in
     Environ.fold_named_context_reverse (fun t decl ->
 					  if is_proof_var decl then
+                                            let decl = Termops.map_named_decl EConstr.of_constr decl in
 					    mkNamedProd_or_LetIn decl t
 					  else
 					    t
-- 
cgit v1.2.3