aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-11 00:29:02 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:27:27 +0100
commitca993b9e7765ac58f70740818758457c9367b0da (patch)
treea813ef9a194638afbb09cefe1d1e2bce113a9d84 /plugins/cc
parentc2855a3387be134d1220f301574b743572a94239 (diff)
Making judgment type generic over the type of inner constrs.
This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/cctac.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 58454eedf..11da923e1 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 }