From 47abea3e05021450743756264c392ec5dc07b97c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 30 Mar 2018 15:59:00 +0200 Subject: Fix #6257: anomaly with Printing Projections and Context. Constrextern.explicitize expected that if implicits were declared they would be declared at least up to the principal argument of the projection, but Context/discharge of implicits does not preserve this. Note the anomaly only happens with primitive projections DISABLED in recent Coqs (>=8.8). Implicit argument experts may consider whether ensuring enough implicits are declared would be better. --- interp/constrextern.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 19444988b..a7c40e9fa 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -590,11 +590,17 @@ let explicitize inctx impl (cf,f) args = let expl () = match ip with | Some i -> - if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then - raise Expl + (* Careful: It is possible to have declared implicits ending + before the principal argument *) + let is_impl = + try is_status_implicit (List.nth impl (i-1)) + with Failure _ -> false + in + if is_impl + then raise Expl else let (args1,args2) = List.chop i args in - let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in + let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in let args1 = exprec 1 (args1,impl1) in let args2 = exprec (i+1) (args2,impl2) in let ip = Some (List.length args1) in -- cgit v1.2.3