wip

LPCIC · Feb 1, 2024 · e0fdfdc · e0fdfdc
1 parent 67e3e89
commit e0fdfdc
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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) } *)