From 6899d3aa567436784a08af4e179c2ef1fa504a02 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 21 Nov 2015 00:17:21 +0100
Subject: Moving extended_rel_vect/extended_rel_list to the kernel.

It will later be used to fix a bug and improve some code.

Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
---
 tactics/extratactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ff1ed40301..0f907b0ef7 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -315,7 +315,7 @@ let project_hint pri l2r r =
     | _ -> assert false in
   let p =
     if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
-  let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in
+  let c = Reductionops.whd_beta Evd.empty (mkApp (c,Context.extended_rel_vect 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
   let id =
-- 
cgit v1.2.3