From e0fdfdc712022c03741020d9cff90a78e88a5329 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Wed, 31 Jan 2024 14:11:53 +0100
Subject: [PATCH] wip

---
 src/coq_elpi_HOAS.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index e1cbc73ff..e729cb862 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -910,6 +910,7 @@ let purge_algebraic_univs_sort state s =
 
 let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) []
 
+(* WIP: I do not know how to make this optional *)
 (* let sort = { sort with API.Conversion.embed = (fun ~depth state s ->
   let state, s = purge_algebraic_univs_sort state (EConstr.ESorts.make s) in
   sort.API.Conversion.embed ~depth state s) } *)