UIP in SProp

2 files changed, 24 insertions, 4 deletions

diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 94d468e640..4023b5a277 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -22,6 +22,11 @@ Module Unsafe.
 
 Ltac2 Type case.
 
+Ltac2 Type case_invert := [
+| NoInvert
+| CaseInvert (instance,constr array)
+].
+
 Ltac2 Type kind := [
 | Rel (int)
 | Var (ident)
@@ -36,7 +41,7 @@ Ltac2 Type kind := [
 | Constant (constant, instance)
 | Ind (inductive, instance)
 | Constructor (constructor, instance)
-| Case (case, constr, constr, constr array)
+| Case (case, constr, case_invert, constr, constr array)
 | Fix (int array, int, binder array, constr array)
 | CoFix (int, binder array, constr array)
 | Proj (projection, constr)
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 0299da6a25..ef666ba9e3 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -107,6 +107,19 @@ let to_rec_declaration (nas, cs) =
   Array.map snd nas,
   Value.to_array Value.to_constr cs)
 
+let of_case_invert = let open Constr in function
+  | NoInvert -> ValInt 0
+  | CaseInvert {univs;args} ->
+    v_blk 0 [|of_instance univs; of_array of_constr args|]
+
+let to_case_invert = let open Constr in function
+  | ValInt 0 -> NoInvert
+  | ValBlk (0, [|univs;args|]) ->
+    let univs = to_instance univs in
+    let args = to_array to_constr args in
+    CaseInvert {univs;args}
+  | _ -> CErrors.anomaly Pp.(str "unexpected value shape")
+
 let of_result f = function
 | Inl c -> v_blk 0 [|f c|]
 | Inr e -> v_blk 1 [|Value.of_exn e|]
@@ -421,10 +434,11 @@ let () = define1 "constr_kind" constr begin fun c ->
       Value.of_ext Value.val_constructor cstr;
       of_instance u;
     |]
-  | Case (ci, c, t, bl) ->
+  | Case (ci, c, iv, t, bl) ->
     v_blk 13 [|
       Value.of_ext Value.val_case ci;
       Value.of_constr c;
+      of_case_invert iv;
       Value.of_constr t;
       Value.of_array Value.of_constr bl;
     |]
@@ -507,12 +521,13 @@ let () = define1 "constr_make" valexpr begin fun knd ->
     let cstr = Value.to_ext Value.val_constructor cstr in
     let u = to_instance u in
     EConstr.mkConstructU (cstr, u)
-  | (13, [|ci; c; t; bl|]) ->
+  | (13, [|ci; c; iv; t; bl|]) ->
     let ci = Value.to_ext Value.val_case ci in
     let c = Value.to_constr c in
+    let iv = to_case_invert iv in
     let t = Value.to_constr t in
     let bl = Value.to_array Value.to_constr bl in
-    EConstr.mkCase (ci, c, t, bl)
+    EConstr.mkCase (ci, c, iv, t, bl)
   | (14, [|recs; i; nas; cs|]) ->
     let recs = Value.to_array Value.to_int recs in
     let i = Value.to_int i in