From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Nov 2016 18:34:53 +0100
Subject: Removing various compatibility layers of tactics.

---
 plugins/romega/refl_omega.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'plugins/romega')

diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index ab5033601a..cfe14b230c 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -740,6 +740,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c =
 
 let reify_gl env gl =
   let concl = Tacmach.pf_concl gl in
+  let concl = EConstr.Unsafe.to_constr concl in
   let t_concl =
     Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in
   if !debug then begin
@@ -748,6 +749,7 @@ let reify_gl env gl =
   end;
   let rec loop = function
       (i,t) :: lhyps ->
+        let t = EConstr.Unsafe.to_constr t in
 	let t' = oproposition_of_constr env (false,[],i,[]) gl t in
 	if !debug then begin
 	  Printf.printf "  %s: " (Names.Id.to_string i);
-- 
cgit v1.2.3