From 1f84b509851f3eead190eac2300ee77611ed9ff4 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 7 Oct 2011 13:57:13 +0000
Subject: 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
---
 pretyping/typeclasses.ml  | 6 ++++--
 pretyping/typeclasses.mli | 2 +-
 2 files changed, 5 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 5447c21458..caee039e0e 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 69a472cb51..e4db68fbcd 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. *)
-- 
cgit v1.2.3