From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 15:50:17 +0100
Subject: Removing some return type compatibility layers in Termops.

---
 ltac/rewrite.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'ltac')

diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index c92ddf9906..a7ff8e1425 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -94,7 +94,6 @@ let find_global dir s =
     fun (evd,cstrs) ->
       let sigma = Sigma.Unsafe.of_evar_map evd in
       let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in
-      let c = EConstr.of_constr c in
       let evd = Sigma.to_evar_map sigma in
 	(evd, cstrs), c
 
@@ -206,7 +205,6 @@ end) = struct
       fun (evd,cstrs) -> 
         let sigma = Sigma.Unsafe.of_evar_map evd in
         let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in
-        let c = EConstr.of_constr c in
         let evd = Sigma.to_evar_map sigma in
 	  (evd, cstrs), c
 	
@@ -215,7 +213,6 @@ end) = struct
       fun (evd,cstrs) -> 
         let sigma = Sigma.Unsafe.of_evar_map evd in
         let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in
-        let c = EConstr.of_constr c in
         let evd = Sigma.to_evar_map sigma in
 	  (evd, cstrs), c
 
-- 
cgit v1.2.3