diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-30 15:59:00 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-30 17:14:13 +0200 |
commit | 47abea3e05021450743756264c392ec5dc07b97c (patch) | |
tree | 3cfdcc4d9597aa9e98caca8ad14497019af03686 /interp/constrextern.ml | |
parent | c0eedb5bdcb815132f404e19d6bf59730ae6e2df (diff) |
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.
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r-- | interp/constrextern.ml | 12 |
1 files changed, 9 insertions, 3 deletions
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 |