From 62789dd765375bef0fb572603aa01039a82dd3b5 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 22 Nov 2012 18:09:23 +0000
Subject: Monomorphization (kernel)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15992 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index b995f2e4a2..3e5b10f3b3 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -180,6 +180,12 @@ type recarg =
   | Mrec of inductive
   | Imbr of inductive
 
+let eq_recarg r1 r2 = match r1, r2 with
+| Norec, Norec -> true
+| Mrec i1, Mrec i2 -> eq_ind i1 i2
+| Imbr i1, Imbr i2 -> eq_ind i1 i2
+| _ -> false
+
 let subst_recarg sub r = match r with
   | Norec -> r
   | Mrec (kn,i) -> let kn' = subst_ind sub kn in
@@ -204,7 +210,7 @@ let dest_recarg p = fst (Rtree.dest_node p)
  *)
 let dest_subterms p =
   let (ra,cstrs) = Rtree.dest_node p in
-  assert (ra<>Norec);
+  assert (match ra with Norec -> false | _ -> true);
   Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs
 
 let recarg_length p j =
-- 
cgit v1.2.3