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

1 files changed, 4 insertions, 4 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 3b2b5d3d4..3551746b8 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) *  *)