Monomorphization (kernel)

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

1 files changed, 5 insertions, 2 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f016a20b7..99b582fe3 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -75,6 +75,9 @@ let update_case_info ci modlist =
 
 let empty_modlist = (Cmap.empty, Mindmap.empty)
 
+let is_empty_modlist (cm, mm) =
+  Cmap.is_empty cm && Mindmap.is_empty mm
+
 let expmod_constr modlist c =
   let rec substrec c =
     match kind_of_term c with
@@ -102,7 +105,7 @@ let expmod_constr modlist c =
   | _ -> map_constr substrec c
 
   in
-  if modlist = empty_modlist then c
+  if is_empty_modlist modlist then c
   else substrec c
 
 let abstract_constant_type =
@@ -136,7 +139,7 @@ let cook_constant env r =
   in
   let const_hyps =
     Sign.fold_named_context (fun (h,_,_) hyps ->
-      List.filter (fun (id,_,_) -> id <> h) hyps)
+      List.filter (fun (id,_,_) -> not (id_eq id h)) hyps)
       hyps ~init:cb.const_hyps in
   let typ = match cb.const_type with
     | NonPolymorphicType t ->