diff options
Diffstat (limited to 'contrib/interface/ascent.mli')
| -rw-r--r-- | contrib/interface/ascent.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 7efed88d6c..65708a191b 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -365,7 +365,6 @@ and ct_INT = CT_int of int and ct_INTRO_PATT = CT_coerce_ID_to_INTRO_PATT of ct_ID - | CT_conj_pattern of ct_INTRO_PATT_LIST * ct_INTRO_PATT_LIST list | CT_disj_pattern of ct_INTRO_PATT_LIST * ct_INTRO_PATT_LIST list and ct_INTRO_PATT_LIST = CT_intro_patt_list of ct_INTRO_PATT list |