diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /plugins/cc/ccalgo.mli | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
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 c72843d5..0dcf3a87 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 *) |