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.
---
 proofs/logic.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index e80f5a64c7..1ba14e7d43 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -13,6 +13,7 @@ open Names
 open Nameops
 open Term
 open Vars
+open Context
 open Termops
 open Environ
 open Reductionops
-- 
cgit v1.2.3