From 57b2637b3f68adba6b8b897eb7a7fbb076b09719 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Fri, 25 Oct 2024 14:59:21 +0200 Subject: [PATCH 1/3] [coq_elpi_builtins] change error msg when loading non-closed clause in a db --- src/coq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 8e3dc692f..02e3babbd 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -579,7 +579,7 @@ let preprocess_clause ~depth clause = E.mkLam (subst ~depth:(depth+1) m x) | E.Builtin(c,xs) -> E.mkBuiltin c (List.map (subst ~depth m) xs) - | E.UnifVar _ -> assert false + | E.UnifVar _ -> CErrors.anomaly Pp.(str"accumulating non-closed clauses is forbidden") | E.Const _ | E.Nil | E.CData _ -> t in let clause = From e91b3c95614f0771af081791f09bb856530d608c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Oct 2024 15:30:11 +0200 Subject: [PATCH 2/3] Update src/coq_elpi_builtins.ml --- src/coq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 02e3babbd..2b6746009 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -579,7 +579,7 @@ let preprocess_clause ~depth clause = E.mkLam (subst ~depth:(depth+1) m x) | E.Builtin(c,xs) -> E.mkBuiltin c (List.map (subst ~depth m) xs) - | E.UnifVar _ -> CErrors.anomaly Pp.(str"accumulating non-closed clauses is forbidden") + | E.UnifVar _ -> CErrors.error Pp.(str"The clause begin accumulated contains unification variables, this is forbidden. You must quantify they out using 'pi'.") | E.Const _ | E.Nil | E.CData _ -> t in let clause = From 66365a9d88ad59b527cc3385889a2c61259a005f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 25 Oct 2024 15:30:35 +0200 Subject: [PATCH 3/3] Update src/coq_elpi_builtins.ml --- src/coq_elpi_builtins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 2b6746009..30cbebf50 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -579,7 +579,7 @@ let preprocess_clause ~depth clause = E.mkLam (subst ~depth:(depth+1) m x) | E.Builtin(c,xs) -> E.mkBuiltin c (List.map (subst ~depth m) xs) - | E.UnifVar _ -> CErrors.error Pp.(str"The clause begin accumulated contains unification variables, this is forbidden. You must quantify they out using 'pi'.") + | E.UnifVar _ -> CErrors.error Pp.(str"The clause begin accumulated contains unification variables, this is forbidden. You must quantify them out using 'pi'.") | E.Const _ | E.Nil | E.CData _ -> t in let clause =