From 47417ac27f539a470e36944b68a8808a0163ddf0 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Wed, 5 Mar 2025 15:58:41 +0100 Subject: [PATCH] give constant to every primitive projection --- src/rocq_elpi_builtins.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 7ceb691ec..f19eac932 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -2363,11 +2363,8 @@ denote the same x as before.|}; MLCode(Pred("coq.env.primitive-projection?", In(projection, "Projection", Out(constant, "Compatibility constant", - Easy "relates a projection to its compatibility constant.")), - (fun p _ ~depth -> - let c = Projection.constant p in - try !: (ignore (Structures.Structure.find_from_projection c); Constant c) - with Not_found -> raise No_clause)), + Easy "relates a primitive projection to its compatibility constant.")), + (fun p _ ~depth -> !: (Constant (Projection.constant p)))), DocAbove); LPDoc "-- Sorts (and their universe level, if applicable) ----------------";