From 95dd7304f68eb155f572bf221c4d99fca85b700c Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 23 Mar 2008 22:11:25 +0000
Subject: 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
---
 parsing/g_vernac.ml4 | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'parsing')

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
-- 
cgit v1.2.3