diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-12 16:06:43 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-12 16:06:43 +0200 |
| commit | 19aa7231ec96dbbfdda7788679cf7ddf00bda7a5 (patch) | |
| tree | 12d614854144384191fb04637498297810020cd9 /pretyping | |
| parent | 827663982e9cdf502f21727677515cf2318aa41d (diff) | |
Minor simplification in evarconv.
Function default_fail was always part of an ise_try. Its associated
error message was anyway thrown away. It is then irrelevant and could
be made simpler.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a39e37444..96c90e2fc 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -362,8 +362,6 @@ let rec evar_conv_x ts env evd pbty term1 term2 = and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = - let default_fail i = (* costly *) - UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) in @@ -415,7 +413,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let not_only_app = Stack.not_purely_applicative skM in let f1 i = match Stack.list_of_app_stack skF with - | None -> default_fail evd + | None -> quick_fail evd | Some lF -> let tM = Stack.zip apprM in miller_pfenning on_left |