diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-06 16:34:11 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-06 16:34:11 +0000 |
| commit | ba360bdefa2d7e4200c94a37c5065019718c2691 (patch) | |
| tree | c9c7362e356add8280035e812d6256874c8fd914 /parsing/ppvernac.ml | |
| parent | d1a73c9a47d554c3cf687f2ed10ace5671d1e6c1 (diff) | |
Fixes in rewrite and a Elimination/Case to Scheme:
- disallow dynamic generation of [case] constructs through [find_scheme]
during a rewrite, as it changes the global environment and subsequent
manipulations of the tactic may use an outdated environment.
- use local exception names so as not to catch and hide unexpected
[Not_found] exceptions.
- fix lifting of constraints for dependent function types
- Allow rewriting on morphisms (terms in function position) even with
[rewrite] (fixes bug #2178).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12848 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppvernac.ml')
| -rw-r--r-- | parsing/ppvernac.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index e88165773..76b52dc33 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -330,6 +330,14 @@ let pr_onescheme (idop,schem) = hov 0 ((if dep then str"Induction for" else str"Minimality for") ++ spc() ++ pr_smart_global ind) ++ spc() ++ hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) + | CaseScheme (dep,ind,s) -> + (match idop with + | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() + | None -> spc () + ) ++ + hov 0 ((if dep then str"Elimination for" else str"Case for") + ++ spc() ++ pr_smart_global ind) ++ spc() ++ + hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) | EqualityScheme ind -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() |