diff options
Diffstat (limited to 'tactics/termdn.ml')
| -rw-r--r-- | tactics/termdn.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 995183dc90..591b2947c9 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -70,6 +70,7 @@ let constr_val_discr t = | Ind ind_sp -> Label(IndRef ind_sp,l) | Construct cstr_sp -> Label((ConstructRef cstr_sp),l) | Var id -> Label(VarRef id,l) + | Const _ -> Everything | _ -> Nothing let constr_val_discr_st (idpred,cpred) t = |