From bfc03c53882d7334e4fb327362c354397a8462ba Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 26 Oct 2008 19:22:27 +0000
Subject: Fixes and refinements regarding occurrence selection: - make the
 modifiers "value of" and "type of" for "set" working (it was not!), - clear
 unselected hypotheses in the "in" clause of "induction/destruct" when   the
 destructed term is a variable (experimental), - support for generalization of
 hypotheses in the induction hypotheses using   the "in" clause of "induction"
 (e.g. "induction n in m, H" will   generalize over m -- would it be better to
 have an explicit   "over"/"generalizing" clause ?). Added clause "as" to
 "apply in".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11509 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 7b654b74b7..26b9be8707 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -7,6 +7,7 @@ open Names;;
 open Ascent;;
 open Genarg;;
 open Rawterm;;
+open Termops;;
 open Tacexpr;;
 open Vernacexpr;;
 open Decl_kinds;;
-- 
cgit v1.2.3