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

1 files changed, 1 insertions, 0 deletions

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;;