From 868b948f8a7bd583d467c5d02dfb34d328d53d37 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 11 Dec 2020 13:20:54 +0100
Subject: Remove redundant univ and parameter info from CaseInvert

---
 user-contrib/Ltac2/Constr.v    |  2 +-
 user-contrib/Ltac2/tac2core.ml | 11 +++++------
 2 files changed, 6 insertions(+), 7 deletions(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 4cc9d99c64..72cac900cd 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -24,7 +24,7 @@ Ltac2 Type case.
 
 Ltac2 Type case_invert := [
 | NoInvert
-| CaseInvert (instance,constr array)
+| CaseInvert (constr array)
 ].
 
 Ltac2 Type kind := [
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 1efbc80e93..64a2b24404 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -109,15 +109,14 @@ let to_rec_declaration (nas, 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|]
+  | CaseInvert {indices} ->
+    v_blk 0 [|of_array of_constr indices|]
 
 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}
+  | ValBlk (0, [|indices|]) ->
+    let indices = to_array to_constr indices in
+    CaseInvert {indices}
   | _ -> CErrors.anomaly Pp.(str "unexpected value shape")
 
 let of_result f = function
-- 
cgit v1.2.3