From 3af8b2cfde3e02075a6b9085b40196658f34fd7b Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Fri, 26 Jan 2024 12:03:26 +0100 Subject: [PATCH] change error msg when section var are cleared --- src/coq_elpi_HOAS.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 8c72470b8..681b0f5d4 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -1306,7 +1306,10 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t = let state, elpi_uvk, _, gsl_t = in_elpi_evar ~calldepth k state in gls := gsl_t @ !gls; let args = Evd.expand_existential sigma (k, args) in - let args = CList.firstn (List.length args - coq_ctx.section_len) args in + let argno = List.length args - coq_ctx.section_len in + if (argno < 0) then + nYI "constr2lp: cleared section variables"; + let args = CList.firstn argno args in let state, args = CList.fold_left_map (aux ~depth env) state args in state, E.mkUnifVar elpi_uvk ~args:(List.rev args) state | C.Sort s -> in_elpi_sort ~depth state (EC.ESorts.kind sigma s)