From c0a71f9ff6289d99bbbcd13ef65c68f74ac9e191 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 12 Feb 2020 10:27:13 +0100 Subject: Remove special case for implicit inductive parameters Co-authored-by: Jasper Hugunin Co-authored-by: Gaëtan Gilbert --- vernac/classes.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 6e929de581..3d38713e09 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -514,7 +514,8 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass = else tclass in let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in - let sigma, (c', imps') = interp_type_evars_impls ~program_mode ~impls env' sigma tclass in + let flags = Pretyping.{ all_no_fail_flags with program_mode } in + let sigma, (c', imps') = interp_type_evars_impls ~flags ~impls env' sigma tclass in let imps = imps @ imps' in let ctx', c = decompose_prod_assum sigma c' in let ctx'' = ctx' @ ctx in -- cgit v1.2.3