diff options
| author | msozeau | 2008-03-23 22:11:25 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-23 22:11:25 +0000 |
| commit | 95dd7304f68eb155f572bf221c4d99fca85b700c (patch) | |
| tree | 8e78cb9ed1eee1939b327cbc0d013f8a99ea4570 /parsing | |
| parent | 32c11b16f7d7ff0ea3aee584103bd60f5b94dedb (diff) | |
Fix a bug found by B. Grégoire when declaring morphisms in module
types. Change (again) the semantics of bindings and the binding modifier
! in typeclasses. Inside [ ], implicit binding where only parameters
need to be given is the default, use ! to use explicit binding, which is
equivalent to regular bindings except for generalization of free
variables. Outside brackets (e.g. on the right of instance
declarations), explicit binding is the default, and implicit binding
can be used by adding ! in front. This avoids almost every use of ! in
the standard library and in other examples I have.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10713 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3b67407311..40c6180f0d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -492,6 +492,11 @@ GEXTEND Gram | 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 *) + let n, bk, t = is in + n, (match bk with Rawterm.Implicit -> Rawterm.Explicit + | Rawterm.Explicit -> Rawterm.Implicit), t + in VernacInstance (sup, is, props, pri) | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is |