diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index e0ae98ffae..0556191be8 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1466,7 +1466,7 @@ let solve_constraints env (evars,cstrs) = (Typeclasses.mark_resolvables ~filter evars) let nf_zeta = - Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) exception RewriteFailure of Pp.std_ppcmds |