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
---
 interp/implicit_quantifiers.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 3b2b5d3d43..3551746b8b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -172,7 +172,7 @@ let full_class_binders env l =
   let l', avoid =
     List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
       match bk with
-	  Explicit -> 
+	  Implicit -> 
 	    let (loc, id, l) = destClassAppExpl cl in
 	    let gr = Nametab.global id in
 	      (try
@@ -180,14 +180,14 @@ let full_class_binders env l =
 		  let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
 		    (iid, bk, CAppExpl (loc, (None, id), args)) :: l', avoid
 		with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
-	| Implicit -> (x :: l', avoid))
+	| Explicit -> (x :: l', avoid))
       ([], avoid) l
   in List.rev l'
       
 let constr_expr_of_constraint (kind, id) l =
   match kind with
-    | Explicit -> CAppExpl (fst id, (None, Ident id), l)
-    | Implicit -> CApp (fst id, (None, CRef (Ident id)),
+    | Implicit -> CAppExpl (fst id, (None, Ident id), l)
+    | Explicit -> CApp (fst id, (None, CRef (Ident id)),
 		       List.map (fun x -> x, None) l)
 
 (*    | CApp of loc * (proj_flag * constr_expr) *  *)
-- 
cgit v1.2.3