💥 Algebraic universes not purged anymore

Author: ecranceMERCE

src/coq_elpi_HOAS.ml

@@ -908,9 +908,9 @@ let purge_algebraic_univs_sort state s =
 
 let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) []
 
-let sort = { sort with API.Conversion.embed = (fun ~depth state s ->
+(* 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) }
+  sort.API.Conversion.embed ~depth state s) } *)
 
 let in_elpi_sort ~depth state s =
   let state, s, gl = sort.API.Conversion.embed ~depth state s in

src/coq_elpi_builtins.ml

@@ -2179,7 +2179,7 @@ phase unnecessary.|};
     | Data u1, Data u2 ->
         if Sorts.equal u1 u2 then state, !: u1 +! u2,[]
         else
-          let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in
+          (* let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in *)
           add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[]
     | _ -> err Pp.(str"coq.sort.leq: called with _ as argument"))),
   DocAbove);
@@ -2193,7 +2193,7 @@ phase unnecessary.|};
     | Data u1, Data u2 ->
       if Sorts.equal u1 u2 then state, !: u1 +! u2,[]
       else
-        let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in
+        (* let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in *)
         add_universe_constraint state (constraint_eq u1 u2), !: u1 +! u2, []
     | _ -> err Pp.(str"coq.sort.eq: called with _ as argument"))),
   DocAbove);