diff options
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 5d286c732..0c5d6ca1f 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -11,7 +11,7 @@ open Term open Names type cinfo = - {ci_constr: constructor; (* inductive type *) + {ci_constr: pconstructor; (* inductive type *) ci_arity: int; (* # args *) ci_nhyps: int} (* # projectable args *) |