diff options
author | 2014-12-16 15:59:52 +0100 | |
---|---|---|
committer | 2014-12-16 16:01:25 +0100 | |
commit | 8029f7555f9c6f201cc70b5ecc538b11a861f0aa (patch) | |
tree | c750b3ea7cafd5ec2176866bbd16208e5335978a /plugins/cc | |
parent | d4f5bdd6f7304fac541bb5f4555ecdd6aa42699a (diff) | |
parent | f88cce2698da000ab9054da31330db70997a41a4 (diff) |
fix bug #2447 in congruence
Diffstat (limited to 'plugins/cc')
-rw-r--r-- | plugins/cc/cctac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 858c80f29..b74b1faca 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -504,8 +504,8 @@ let f_equal = end | _ -> Proofview.tclUNIT () end - begin function + begin function (e, info) -> match e with | Type_errors.TypeError _ -> Proofview.tclUNIT () - | e -> Proofview.tclZERO e + | e -> Proofview.tclZERO ~info e end end |