diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-04 16:55:36 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-04 16:55:36 +0200 |
commit | b7aa3064e50e34afe2e1a458f61e6e2b1f5d37f8 (patch) | |
tree | 9198a8c2f4f1a62ac7e661365685fbb496950ada /interp/constrextern.ml | |
parent | f95d33479cae45a5f6f18eb260e3c9ffcb605882 (diff) | |
parent | 47abea3e05021450743756264c392ec5dc07b97c (diff) |
Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.
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 48ddd9496..bb5fd5294 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -589,11 +589,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 |