diff options
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/constrintern.mli | 2 | ||||
| -rw-r--r-- | test-suite/success/ImplicitArguments.v | 5 | ||||
| -rw-r--r-- | vernac/command.ml | 4 |
4 files changed, 10 insertions, 5 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4dcf287ef..3dfc85041 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -190,10 +190,10 @@ let compute_internalization_data env ty typ impl = let expls_impl = compute_explicitable_implicit impl ty in (ty, expls_impl, impl, compute_arguments_scope typ) -let compute_internalization_env env ty = +let compute_internalization_env env ?(impls=empty_internalization_env) ty = List.fold_left3 (fun map id typ impl -> Id.Map.add id (compute_internalization_data env ty typ impl) map) - empty_internalization_env + impls (**********************************************************************) (* Contracting "{ _ }" in notations *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 644cafe57..f3306b592 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -61,7 +61,7 @@ val empty_internalization_env : internalization_env val compute_internalization_data : env -> var_internalization_type -> types -> Impargs.manual_explicitation list -> var_internalization_data -val compute_internalization_env : env -> var_internalization_type -> +val compute_internalization_env : env -> ?impls:internalization_env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index f07773f8b..921433cad 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -27,3 +27,8 @@ Parameters (a:_) (b:a=0). Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl. Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat. + +(* Some example which should succeed with local implicit arguments *) + +Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A. +Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P. diff --git a/vernac/command.ml b/vernac/command.ml index e2ebb4d7f..02d852515 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -582,7 +582,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let pl = (List.hd indl).ind_univs in let ctx = Evd.make_evar_universe_context env0 pl in let evdref = ref Evd.(from_ctx ctx) in - let _, ((env_params, ctx_params), userimpls) = + let impls, ((env_params, ctx_params), userimpls) = interp_context_evars env0 evdref paramsl in let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in @@ -603,7 +603,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = let indimpls = List.map (fun (_, _, impls) -> userimpls @ lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in - let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in + let impls = compute_internalization_env env0 ~impls (Inductive params) indnames fullarities indimpls in let implsforntn = compute_internalization_env env0 Variable indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in |