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

2 files changed, 20 insertions, 6 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index a77fc57413..aa6cc297b3 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -673,10 +673,18 @@ let subst_term_occ (nowhere_except_in,locs as plocs) c t =
     if rest <> [] then error_invalid_occurrence rest;
     t'
 
-let subst_term_occ_decl (nowhere_except_in,locs as plocs) c (id,bodyopt,typ as d) =
-  match bodyopt with
-    | None -> (id,None,subst_term_occ plocs c typ)
-    | Some body -> 
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+  | InHyp
+  | InHypTypeOnly
+  | InHypValueOnly
+
+let subst_term_occ_decl ((nowhere_except_in,locs as plocs),hloc) c (id,bodyopt,typ as d) =
+  match bodyopt,hloc with
+  | None, InHypValueOnly -> errorlabstrm "" (pr_id id ++ str " has no value")
+  | None, _ -> (id,None,subst_term_occ plocs c typ)
+  | Some body, InHypTypeOnly -> (id,Some body,subst_term_occ plocs c typ)
+  | Some body, InHypValueOnly -> (id,Some (subst_term_occ plocs c body),typ)
+  | Some body, InHyp ->
 	if locs = [] then
 	  if nowhere_except_in then d
 	  else (id,Some (subst_term c body),subst_term c typ)
@@ -687,7 +695,6 @@ let subst_term_occ_decl (nowhere_except_in,locs as plocs) c (id,bodyopt,typ as d
 	  if rest <> [] then error_invalid_occurrence rest;
 	  (id,Some body',t')
 
-
 (* First character of a constr *)
 
 let lowercase_first_char id =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index e9516ec486..92c0a78d48 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -150,8 +150,15 @@ val subst_term_occ : occurrences -> constr -> constr -> constr
 
 (* [subst_term_occ_decl occl c decl] replaces occurrences of [c] at
    positions [occl] by [Rel 1] in [decl] *)
+
+type hyp_location_flag = (* To distinguish body and type of local defs *)
+  | InHyp
+  | InHypTypeOnly
+  | InHypValueOnly
+
 val subst_term_occ_decl :
-  occurrences -> constr -> named_declaration -> named_declaration
+  occurrences * hyp_location_flag -> constr -> named_declaration -> 
+      named_declaration
 
 val error_invalid_occurrence : int list -> 'a