diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-30 21:42:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-30 21:42:58 +0000 |
| commit | 90e5407fcfc59dce5ea592aeae6195183a2b4ad2 (patch) | |
| tree | a30c7aebc8d840b87d702b972fbbff16714e4b6d /parsing | |
| parent | 0b6924f05ef6beb775345f3fb2ad21a009ab3baa (diff) | |
Ajout d'abbréviations/notations paramétriques
Example: "Notation reflexive R := (forall x, R x x)."
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 6 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 7 |
3 files changed, 10 insertions, 8 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index df29d5096..a693ebdb5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -794,9 +794,10 @@ GEXTEND Gram modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (local,(op,modl),p,sc) - | IDENT "Notation"; local = locality; id = ident; ":="; c = constr; + | IDENT "Notation"; local = locality; id = ident; idl = LIST0 ident; + ":="; c = constr; b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] -> - VernacSyntacticDefinition (id,c,local,b) + VernacSyntacticDefinition (id,(idl,c),local,b) | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 7ca1964ea..a013b4b93 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -816,10 +816,10 @@ let rec pr_vernac = function prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr pr_pattern_expr - | VernacSyntacticDefinition (id,c,local,onlyparsing) -> + | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) -> hov 2 - (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++ - pr_constrarg c ++ + (str"Notation " ++ pr_locality local ++ pr_id id ++ + prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) | VernacDeclareImplicits (local,q,e,None) -> hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q) diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 767072e2b..7eb8a538b 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -400,11 +400,12 @@ let gallina_print_constant_with_infos sp = let gallina_print_syntactic_def kn = let sep = " := " and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn - and c = Syntax_def.search_syntactic_definition dummy_loc kn in - str "Notation " ++ pr_qualid qid ++ str sep ++ + and (vars,a) = Syntax_def.search_syntactic_definition dummy_loc kn in + let c = Topconstr.rawconstr_of_aconstr dummy_loc a in + str "Notation " ++ pr_qualid qid ++ + prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++ Constrextern.without_symbols pr_lrawconstr c ++ fnl () - let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " and tag = object_tag lobj in |