diff options
| author | msozeau | 2009-10-27 19:43:51 +0000 |
|---|---|---|
| committer | msozeau | 2009-10-27 19:43:51 +0000 |
| commit | 36c448f43c7fa16163b543b941be4a917a712a37 (patch) | |
| tree | 73affd4fede1fea0dd56a2600bc420de769432e2 /parsing | |
| parent | 3178c7a29ff8b57a4598c4c5ded2eb29b8067dcf (diff) | |
Add a new vernacular command for controling implicit generalization of
variables with syntax:
[Local?|Global] Generalizable Variable(s)? [all|none|id1 idn].
By default no variable is generalizable, so this patch breaks backward
compatibility with files that used implicit generalization (through
Instance declarations for example). To get back the old behavior, one
just needs to use [Global Generalizable Variables all].
Make coq_makefile more robust using [mkdir -p].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 11 |
2 files changed, 17 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e1a71ff23f..52cb3d8989 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -518,7 +518,7 @@ GEXTEND Gram pri = OPT [ "|"; i = natural -> i ] ; props = [ ":="; "{"; r = record_declaration; "}" -> r | ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] -> - VernacInstance (not (use_non_locality ()), [], ((loc,Anonymous), expl, t), props, pri) + VernacInstance (not (use_section_locality ()), [], ((loc,Anonymous), expl, t), props, pri) | IDENT "Instance"; name = identref; sup = OPT binders_let; ":"; expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200"; @@ -545,7 +545,12 @@ GEXTEND Gram VernacDeclareImplicits (use_section_locality (),qid,pos) | IDENT "Implicit"; ["Type" | IDENT "Types"]; - idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ] + idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) + + | IDENT "Generalizable"; ["Variable" | IDENT "Variables"]; + gen = [ IDENT "none" -> None | IDENT "all" -> Some [] | + idl = LIST1 identref -> Some idl ] -> + VernacGeneralizable (use_section_locality (), gen) ] ] ; implicit_name: [ [ "!"; id = ident -> (id, false, true) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 76098e4fb1..8a8248bf4c 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -831,7 +831,8 @@ let rec pr_vernac = function (pr_locality local ++ str "Ltac " ++ prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) | VernacCreateHintDb (local,dbname,b) -> - hov 1 (pr_locality local ++ str "Create " ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ())) + hov 1 (pr_locality local ++ str "Create " ++ str "HintDb " ++ + str dbname ++ (if b then str" discriminated" else mt ())) | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr pr_constr_pattern_expr | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) -> @@ -851,6 +852,14 @@ let rec pr_vernac = function str (if List.length idl > 1 then "s " else " ") ++ prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_lconstr c) + | VernacGeneralizable (local, g) -> + hov 1 (pr_locality local ++ str"Generalizable Variable" ++ + match g with + | None -> str "s none" + | Some [] -> str "s all" + | Some idl -> + str (if List.length idl > 1 then "s " else " ") ++ + prlist_with_sep spc pr_lident idl) | VernacSetOpacity(b,[k,l]) when k=Conv_oracle.transparent -> hov 1 (str"Transparent" ++ pr_non_locality b ++ spc() ++ prlist_with_sep sep pr_smart_global l) |