From d96ec0f0a094ce84890297be342bc129d0d6b47b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 28 Oct 2009 16:05:59 +0000
Subject: Backport fix for indexing of sorts which collapse every Type
 occurrence into a SortLabel None.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12434 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/btermdn.ml | 41 +++++++++++++++++++++--------------------
 1 file changed, 21 insertions(+), 20 deletions(-)

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 198ee78595..bcb9a411c0 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -62,26 +62,27 @@ struct
       decrec []
 
   let constr_val_discr t =
-  let c, l = decomp t in
-    match kind_of_term c with
-    | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
-    | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
-    | Var id -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
-    | Const _ -> Dn.Everything
-    | _ -> Dn.Nothing
-
-let constr_val_discr_st (idpred,cpred) t =
-  let c, l = decomp t in
-    match kind_of_term c with
-    | Const c -> if Cpred.mem c cpred then Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l)
-    | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
-    | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
-    | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
-    | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
-    | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
-    | Sort s -> Dn.Label(Term_dn.SortLabel (Some s), [])
-    | Evar _ -> Dn.Everything
-    | _ -> Dn.Nothing
+    let c, l = decomp t in
+      match kind_of_term c with
+      | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
+      | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
+      | Var id -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
+      | Const _ -> Dn.Everything
+      | _ -> Dn.Nothing
+	
+  let constr_val_discr_st (idpred,cpred) t =
+    let c, l = decomp t in
+      match kind_of_term c with
+      | Const c -> if Cpred.mem c cpred then Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l)
+      | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
+      | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
+      | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
+      | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
+      | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
+      | Sort s when is_small s -> Dn.Label(Term_dn.SortLabel (Some s), [])
+      | Sort _ -> Dn.Label(Term_dn.SortLabel None, [])
+      | Evar _ -> Dn.Everything
+      | _ -> Dn.Nothing
 
   let bounded_constr_pat_discr_st st (t,depth) =
     if depth = 0 then 
-- 
cgit v1.2.3