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
---
 contrib/subtac/subtac_classes.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib')

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 39865f1f9f..0c99fe16ec 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -107,7 +107,7 @@ let new_instance ctx (instid, bk, cl) props pri =
   let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in
   let tclass =
     match bk with
-      | Explicit ->
+      | Implicit ->
 	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
 	  let k = class_info (Nametab.global id) in
 	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
@@ -128,7 +128,7 @@ let new_instance ctx (instid, bk, cl) props pri =
 	      par (List.rev k.cl_context)
 	    in Topconstr.CAppExpl (loc, (None, id), pars)
 
-      | Implicit -> cl
+      | Explicit -> cl
   in
   let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in
   let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in
-- 
cgit v1.2.3