diff options
| -rw-r--r-- | interp/constrextern.ml | 12 | ||||
| -rw-r--r-- | test-suite/output/Projections.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Projections.v | 11 |
3 files changed, 22 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 48ddd94961..bb5fd5294f 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 diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out new file mode 100644 index 0000000000..e9c28faf1d --- /dev/null +++ b/test-suite/output/Projections.out @@ -0,0 +1,2 @@ +fun S : store => S.(store_funcs) + : store -> host_func diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v new file mode 100644 index 0000000000..098a518dc4 --- /dev/null +++ b/test-suite/output/Projections.v @@ -0,0 +1,11 @@ + +Set Printing Projections. + +Class HostFunction := host_func : Type. + +Section store. + Context `{HostFunction}. + Record store := { store_funcs : host_func }. +End store. + +Check (fun (S:@store nat) => S.(store_funcs)). |