diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-28 16:05:59 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-28 16:05:59 +0000 |
| commit | d96ec0f0a094ce84890297be342bc129d0d6b47b (patch) | |
| tree | b81545e0083f2e99575ef0f6afab16644e0a98cd /tactics/btermdn.ml | |
| parent | 4629099adffd33f1c4aaa4bb7866d7f3e58f07cd (diff) | |
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
Diffstat (limited to 'tactics/btermdn.ml')
| -rw-r--r-- | tactics/btermdn.ml | 41 |
1 files changed, 21 insertions, 20 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 198ee7859..bcb9a411c 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 |