aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/interface/xlate.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 9c81a1c3a..af68c7cf9 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -416,7 +416,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
CT_coerce_ID_to_FORMULA(CT_metaid (string_of_id s))
| CPatVar (_, (true, s)) ->
xlate_error "Second order variable not supported"
- | CEvar (_, _) -> xlate_error "CEvar not supported"
+ | CEvar _ -> xlate_error "CEvar not supported"
| CCoFix (_, (_, id), lm::lmi) ->
let strip_mutcorec (fid, bl,arf, ardef) =
CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,