give constant to every primitive projection

LPCIC · Mar 5, 2025 · 47417ac · 47417ac
1 parent 5cd165a
commit 47417ac
Showing 1 changed file with 2 additions and 5 deletions.
diff --git 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) ----------------";