diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-26 19:22:27 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-26 19:22:27 +0000 |
| commit | bfc03c53882d7334e4fb327362c354397a8462ba (patch) | |
| tree | 7e092b31a5e28a38ab973bcc8325a30f7445af36 /pretyping/termops.ml | |
| parent | c52c9cb2655b600f19f37a4636ed4732639e69e7 (diff) | |
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
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index a77fc5741..aa6cc297b 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 = |