Fixpoints are traverse during implicits arguments search to toplevel

registration (& CHANGES update)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13826 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 2 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index ae173f6c3..90376a431 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -68,13 +68,14 @@ let interp_definition bl red_option c ctypopt =
   let env = Global.env() in
   let evdref = ref Evd.empty in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars evdref env bl in
+  let nb_args = List.length ctx in
   let imps,ce =
     match ctypopt with
       None ->
 	let c, imps2 = interp_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c in
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	check_evars env Evd.empty !evdref body;
-	imps1@imps2,
+	imps1@(Impargs.lift_implicits nb_args imps2),
 	{ const_entry_body = body;
 	  const_entry_type = None;
           const_entry_opaque = false }
@@ -85,7 +86,7 @@ let interp_definition bl red_option c ctypopt =
 	let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
 	check_evars env Evd.empty !evdref body;
 	check_evars env Evd.empty !evdref typ;
-	imps1@imps2,
+	imps1@(Impargs.lift_implicits nb_args imps2),
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
           const_entry_opaque = false }