Monomorphization (library)

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

1 files changed, 2 insertions, 2 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 7364031d52..9d986d185a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -128,7 +128,7 @@ let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
   let _,dir,_ = repr_kn kn in
   check_exists sp;
   let kn' = Global.add_constant dir id cdt in
-  assert (kn' = constant_of_kn kn);
+  assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   add_section_constant kn' (Global.lookup_constant kn').const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
@@ -235,7 +235,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   let kn' = Global.add_mind dir id mie in
-  assert (kn'= mind_of_kn kn);
+  assert (eq_mind kn' (mind_of_kn kn));
   add_section_kn kn' (Global.lookup_mind kn').mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names;