diff options
Diffstat (limited to 'pretyping/cbv.mli')
| -rw-r--r-- | pretyping/cbv.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 3ee7bebf0..5f9609a5c 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -24,7 +24,7 @@ val cbv_norm : cbv_infos -> constr -> constr (*********************************************************************** i This is for cbv debug *) -open Term +open Constr type cbv_value = | VAL of int * constr |