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, 2 insertions, 2 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index b3d76b89b..e798d8755 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -530,13 +530,13 @@ let compute_bl_tact ind lnamesparrec nparrec  =
                       tclORELSE reflexivity (Equality.discr_tac false None)
                      );
                      simpl_in_hyp
-		       ((Rawterm.all_occurrences_expr,freshz),Tacexpr.InHyp);
+		       ((Rawterm.all_occurrences_expr,freshz),InHyp);
 (*
 repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 *)
                     tclREPEAT (
                       tclTHENSEQ [
-                         apply_in false freshz [(andb_prop()),Rawterm.NoBindings];
+                         apply_in false freshz [(andb_prop()),Rawterm.NoBindings] None;
                          fun gl ->
                            let fresht = fresh_id (!avoid) (id_of_string "Z") gsig 
                            in