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.
---
 plugins/fourier/fourierR.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index ec73fccb5b..e11cbc279a 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -190,6 +190,8 @@ type hineq={hname:constr; (* le nom de l'hypothèse *)
 exception NoIneq
 
 let ineq1_of_constr (h,t) =
+  let h = EConstr.Unsafe.to_constr h in
+  let t = EConstr.Unsafe.to_constr t in
     match (kind_of_term t) with
       | App (f,args) ->
         (match kind_of_term f with
@@ -504,7 +506,7 @@ let rec fourier () =
         |_-> raise GoalDone
      with GoalDone ->
     (* les hypothèses *)
-    let hyps = List.map (fun (h,t)-> (mkVar h,t))
+    let hyps = List.map (fun (h,t)-> (EConstr.mkVar h,t))
                         (list_of_sign (Proofview.Goal.hyps gl)) in
     let lineq =ref [] in
     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
-- 
cgit v1.2.3