diff options
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 6068cd90f1..0d7ba69955 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -197,7 +197,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = let fixtypes = List.map2 build_fix_type fixctxs fixccls in let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in let fiximps = List.map3 - (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps)) + (fun ctximps cclimps (_,ctx) -> ctximps@cclimps) fixctximps fixcclimps fixctxs in let sigma, rec_sign = List.fold_left2 |