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.

---
 plugins/funind/recdef.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/funind/recdef.ml')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c71174fefb..23b308efbe 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -408,6 +408,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
 		args.(1),args.(2)
 	      in
 	      let new_b' = Termops.replace_term (project g') (EConstr.of_constr teq_lhs) (EConstr.of_constr teq_rhs) (EConstr.of_constr new_b) in 
+	      let new_b' = EConstr.Unsafe.to_constr new_b' in
 	      let new_infos = {
 		infos with 
 		  info = new_b';
@@ -1253,7 +1254,7 @@ let clear_goals =
       | Prod(Name id as na,t',b) ->
 	  let b' = clear_goal b in
 	  if noccurn 1 b' && (is_rec_res id)
-	  then Termops.pop (EConstr.of_constr b')
+	  then Vars.lift (-1) b'
 	  else if b' == b then t
 	  else mkProd(na,t',b')
       | _ -> Term.map_constr clear_goal t
-- 
cgit v1.2.3