From d72e5c154faeea1d55387bc8c039d97f63ebd1c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 Mar 2019 21:03:37 +0100
Subject: Change the representation of kernel case.

We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
---
 user-contrib/Ltac2/tac2core.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 8663691c0a..1efbc80e93 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -378,6 +378,7 @@ end
 let () = define1 "constr_kind" constr begin fun c ->
   let open Constr in
   Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.tclENV >>= fun env ->
   return begin match EConstr.kind sigma c with
   | Rel n ->
     v_blk 0 [|Value.of_int n|]
@@ -434,7 +435,9 @@ let () = define1 "constr_kind" constr begin fun c ->
       Value.of_ext Value.val_constructor cstr;
       of_instance u;
     |]
-  | Case (ci, c, iv, t, bl) ->
+  | Case (ci, u, pms, c, iv, t, bl) ->
+    (* FIXME: also change representation Ltac2-side? *)
+    let (ci, c, iv, t, bl) = EConstr.expand_case env sigma (ci, u, pms, c, iv, t, bl) in
     v_blk 13 [|
       Value.of_ext Value.val_case ci;
       Value.of_constr c;
@@ -472,6 +475,8 @@ let () = define1 "constr_kind" constr begin fun c ->
 end
 
 let () = define1 "constr_make" valexpr begin fun knd ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.tclENV >>= fun env ->
   let c = match Tac2ffi.to_block knd with
   | (0, [|n|]) ->
     let n = Value.to_int n in
@@ -529,7 +534,7 @@ let () = define1 "constr_make" valexpr begin fun knd ->
     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, iv, t, bl)
+    EConstr.mkCase (EConstr.contract_case env sigma (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
-- 
cgit v1.2.3


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