From f2da732ffd5db2b93a2c8120c668f8b2f6068d3b Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 7 Dec 1999 14:56:36 +0000
Subject: debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas
 linkes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@220 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 8a2974f6c8..9542dba9f8 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -90,3 +90,5 @@ val find_case_dep_nparams :
 val type_inst_construct : env -> 'a evar_map -> int -> constr -> constr 
 
 val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool
+
+val keep_hyps : var_context -> Idset.t -> var_context
-- 
cgit v1.2.3