diff options
Diffstat (limited to 'tactics/termdn.mli')
| -rw-r--r-- | tactics/termdn.mli | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/tactics/termdn.mli b/tactics/termdn.mli index 92a1b8c3ea..f3743b1280 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -48,12 +48,18 @@ val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit (*i*) (* These are for Nbtermdn *) +type term_label = + | GRLabel of global_reference + | ProdLabel + | LambdaLabel + | SortLabel of sorts option + val constr_pat_discr_st : transparent_state -> - constr_pattern -> (global_reference * constr_pattern list) option + constr_pattern -> (term_label * constr_pattern list) option val constr_val_discr_st : transparent_state -> - constr -> (global_reference * constr list) Dn.lookup_res + constr -> (term_label * constr list) Dn.lookup_res -val constr_pat_discr : constr_pattern -> (global_reference * constr_pattern list) option -val constr_val_discr : constr -> (global_reference * constr list) Dn.lookup_res +val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option +val constr_val_discr : constr -> (term_label * constr list) Dn.lookup_res (*i*) |