diff options
| author | msozeau | 2008-04-15 13:19:33 +0000 |
|---|---|---|
| committer | msozeau | 2008-04-15 13:19:33 +0000 |
| commit | 44e7deb7c82ec2ddddf551a227c67a76ccb3009a (patch) | |
| tree | 1f5b7f0b0684059930e0567b2cecc194c1869aec /parsing | |
| parent | 07e03e167c7eda30ffc989530470b5c597beaedc (diff) | |
- Add "Global" modifier for instances inside sections with the usual
semantics.
- Add an Equivalence instance for pointwise equality from an
Equivalence on the codomain of a function type, used by default when
comparing functions with the Setoid's ===/equiv.
- Partially fix the auto hint database "add" function where the exact
same lemma could be added twice (happens when doing load for example).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10797 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 3 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 2 |
3 files changed, 6 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 45c16a1335..aea0cf27b5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -489,7 +489,8 @@ GEXTEND Gram | IDENT "Context"; c = typeclass_context -> VernacContext c - | IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ]; + | global = [ IDENT "Global" -> true | -> false ]; + IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ]; is = typeclass_constraint ; pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs -> let sup = match sup with None -> [] | Some l -> l in let is = (* We reverse the default binding mode on the right *) @@ -497,7 +498,7 @@ GEXTEND Gram n, (match bk with Rawterm.Implicit -> Rawterm.Explicit | Rawterm.Explicit -> Rawterm.Implicit), t in - VernacInstance (sup, is, props, pri) + VernacInstance (global, sup, is, props, pri) | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index a013b4b93d..9fe24f4d40 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -706,8 +706,9 @@ let rec pr_vernac = function prlist_with_sep (fun () -> str";" ++ spc()) (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) - | VernacInstance (sup, (instid, bk, cl), props, pri) -> + | VernacInstance (glob, sup, (instid, bk, cl), props, pri) -> hov 1 ( + pr_non_globality (not glob) ++ str"Instance" ++ spc () ++ pr_and_type_binders_arg sup ++ str"=>" ++ spc () ++ diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 396cc63184..48fe40cab2 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -773,7 +773,7 @@ let print_typeclasses () = let pr_instance env i = (* gallina_print_constant_with_infos i.is_impl *) (* lighter *) - print_ref false (ConstRef i.is_impl) + print_ref false (ConstRef (instance_impl i)) let print_instances r = let env = Global.env () in |