From 8aee85814c81486bd3260eff83b0d70c64568748 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Fri, 29 Nov 2024 16:50:54 +0100
Subject: [PATCH] WIP

---
 src/ecLowGoal.ml | 40 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 39 insertions(+), 1 deletion(-)

diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml
index e8c8ec440..f1ccd1d11 100644
--- a/src/ecLowGoal.ml
+++ b/src/ecLowGoal.ml
@@ -1536,9 +1536,47 @@ let t_split_and_i (i : int) (f : form) (tc : tcenv1) =
 
     doit fsl in
 
+  let tc = FApi.tcenv_of_tcenv1 tc in
+  let tc, gl = FApi.newgoal tc fsl in
+  let tc, gr = FApi.newgoal tc fsr in
+
+  tc
+
+  (*
+(* -------------------------------------------------------------------- *)
+require import AllCore.
+
+lemma test : forall a b c d, a && (b /\ (c /\ d)).
+proof.
+move => *.
+split 1.
+admit.
+
+gl = a && b
+gr = c /\ d
+
+proja2 gl = b
+
+conja (proja1 gl) (conj (proja2 gl) gr) = a && (b /\ (c /\ d))
+
+
+
+admit.
+
+
+
+admit.
+
+
+
+
+abort.
+
+
+
   FApi.xmutate1
     tc (fun hd -> VConv (hd, Sid.empty)) [fsl; fsr]
-
+*)
 
 (*
   if i <= 0 then begin