diff options
| author |  Pierre Corbineau <Pierre.Corbineau@NOSPAM@imag.fr> | 2014-12-16 15:59:52 +0100 |
|---|---|---|
| committer | Pierre Corbineau <Pierre.Corbineau@NOSPAM@imag.fr> | 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 |