Use Constr.is_proj for checking projections (#110)

mit-plv · Sep 19, 2023 · f7955ba · f7955ba
1 parent b1d8025
commit f7955ba
Showing 1 changed file with 4 additions and 3 deletions.
diff --git a/src/Rewriter/Language/Reify.v b/src/Rewriter/Language/Reify.v
@@ -422,9 +422,10 @@ Module Compilers.
         => do_red ()
       | Constr.Unsafe.Case _ _ _ _ _
         => do_red ()
-      | Constr.Unsafe.Proj _ _
-        => do_red ()
-      | _ => false
+      | _ (* use ifs for more version-compatibility as the kind representation changes *)
+        => if Constr.is_proj parameter_type
+           then do_red ()
+           else false
       end.
 
     (* f, f_ty, arg *)