diff options
| author | msozeau | 2010-03-06 16:34:11 +0000 |
|---|---|---|
| committer | msozeau | 2010-03-06 16:34:11 +0000 |
| commit | ba360bdefa2d7e4200c94a37c5065019718c2691 (patch) | |
| tree | c9c7362e356add8280035e812d6256874c8fd914 /parsing | |
| 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')
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 8 |
2 files changed, 12 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2eec7848ae..a153762ced 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -298,6 +298,10 @@ GEXTEND Gram IDENT "Sort"; s = sort-> InductionScheme(true,ind,s) | IDENT "Minimality"; "for"; ind = smart_global; IDENT "Sort"; s = sort-> InductionScheme(false,ind,s) + | IDENT "Elimination"; "for"; ind = smart_global; + IDENT "Sort"; s = sort-> CaseScheme(true,ind,s) + | IDENT "Case"; "for"; ind = smart_global; + IDENT "Sort"; s = sort-> CaseScheme(false,ind,s) | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ] ; (* Various Binders *) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index e881657734..76b52dc33e 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() |