Fix bug #2557 and an issue with Propers for complement

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14523 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 9 insertions, 7 deletions

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 9fc3cb59c..000ffc622 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -166,7 +166,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	in
 	let app, ty_constr = instance_constructor k subst in
 	let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-	let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in
+	let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
 	  term, termtype
     | Inr def ->
 	let termtype = it_mkProd_or_LetIn cty ctx in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 5447c2145..caee039e0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -337,9 +337,11 @@ let instance_constructor cl args =
   let lenpars = List.length (List.filter (fun (na, b, t) -> b = None) (snd cl.cl_context)) in
   let pars = fst (list_chop lenpars args) in
     match cl.cl_impl with
-      | IndRef ind -> applistc (mkConstruct (ind, 1)) args,
+      | IndRef ind -> Some (applistc (mkConstruct (ind, 1)) args),
 	  applistc (mkInd ind) pars
-      | ConstRef cst -> list_last args, applistc (mkConst cst) pars
+      | ConstRef cst -> 
+	let term = if args = [] then None else Some (list_last args) in
+	  term, applistc (mkConst cst) pars
       | _ -> assert false
 
 let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 69a472cb5..e4db68fbc 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -73,7 +73,7 @@ val is_implicit_arg : hole_kind -> bool
 (** Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
 
-val instance_constructor : typeclass -> constr list -> constr * types
+val instance_constructor : typeclass -> constr list -> constr option * types
 
 (** Resolvability.
     Only undefined evars could be marked or checked for resolvability. *)
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 9a555e256..f798ad68a 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -236,7 +236,7 @@ Program Definition complement_proper
     intuition.
   Qed.
  
-Hint Extern 1 (Proper (_ ==> _ ==> iff) (complement _)) => 
+Hint Extern 1 (Proper (_ ==> _ ==> _) (complement _)) => 
   apply @complement_proper : typeclass_instances.
 
 (** The [inverse] too, actually the [flip] instance is a bit more general. *)
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index d6e88ed2c..34ecab2d5 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -190,7 +190,7 @@ let declare_class_instance gr ctx params =
   let ident = make_instance_ident gr in
   let cl = Typeclasses.class_info gr in
   let (def,typ) = Typeclasses.instance_constructor cl params in
-  let (def,typ) = it_mkLambda_or_LetIn def ctx, it_mkProd_or_LetIn typ ctx in
+  let (def,typ) = it_mkLambda_or_LetIn (Option.get def) ctx, it_mkProd_or_LetIn typ ctx in
   let def = deep_refresh_universes def in
   let typ = deep_refresh_universes typ in
   let ce = Entries.DefinitionEntry
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 46dea6dc0..55c68d3ce 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -243,7 +243,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	      in
 	      let app, ty_constr = instance_constructor k subst in
 	      let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-	      let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in
+	      let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
 		Some term, termtype
 	  | Some (Inr (def, subst)) ->
 	      let termtype = it_mkProd_or_LetIn cty ctx in