diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/cc/cctac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 58454eedfe..11da923e18 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -512,7 +512,7 @@ let f_equal = | _ -> Proofview.tclUNIT () end begin function (e, info) -> match e with - | Type_errors.TypeError _ -> Proofview.tclUNIT () + | Pretype_errors.PretypeError _ | Type_errors.TypeError _ -> Proofview.tclUNIT () | e -> Proofview.tclZERO ~info e end end } |