From e034b4090ca45410853db60ae2a5d2f220b48792 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 May 2019 19:21:49 +0200
Subject: Turning "manual_implicits" into a list of position in impargs.ml.

---
 vernac/comFixpoint.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comFixpoint.ml')

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
-- 
cgit v1.2.3