diff options
| author | Hugo Herbelin | 2019-05-25 19:21:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-16 14:04:19 +0200 |
| commit | e034b4090ca45410853db60ae2a5d2f220b48792 (patch) | |
| tree | c6f3476741850b4092c789f8bc9c8b3b2940b29d /vernac/comFixpoint.ml | |
| parent | f95017c2c69ee258ae570b789bce696357d2c365 (diff) | |
Turning "manual_implicits" into a list of position in impargs.ml.
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 |