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/decl_mode/decl_interp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index ddf0137354..ae057b4581 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -374,7 +374,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
     match st'.st_it with
 	Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label}
       | This _ -> {st_it = This st.st_it;st_label=st.st_label} in
-  let thyps = fst (match_hyps blend nam2 (Termops.pop (EConstr.of_constr rest1)) hyps) in
+  let thyps = fst (match_hyps blend nam2 (Vars.lift (-1) rest1) hyps) in
     tparams,{pat_vars=tpatvars;
 	     pat_aliases=taliases;
 	     pat_constr=pat_pat;
-- 
cgit v1.2.3