diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-23 16:14:28 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:10 +0200 |
| commit | 72c6588923dca52be7bc7d750d969ff1baa76c45 (patch) | |
| tree | a8b46ecadae6fcf29b6c3dd504e557dfea444f4e /plugins/cc/ccalgo.mli | |
| parent | 26628315688e07c43b9881872a737454e93fe4c9 (diff) | |
Univs: fix an evar leak in congruence
Diffstat (limited to 'plugins/cc/ccalgo.mli')
| -rw-r--r-- | plugins/cc/ccalgo.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index c72843d55..0dcf3a870 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -30,7 +30,7 @@ type cinfo = type term = Symb of constr - | Product of sorts_family * sorts_family + | Product of sorts * sorts | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) |