Changing to an opaq record in BTL info, this is a broken commit

1 files changed, 7 insertions, 7 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 94d299e7..cd69cd37 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -557,21 +557,21 @@ Qed.
 Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
   match i with
   | Bgoto pc => Sgoto pc
-  | Bcall sig ros args res pc _ => 
+  | Bcall sig ros args res pc => 
     let svos := sum_left_map sis.(si_sreg) ros in
     let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
     Scall sig svos sargs res pc
-  | Btailcall sig ros args _ =>
+  | Btailcall sig ros args =>
     let svos := sum_left_map sis.(si_sreg) ros in
     let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
     Stailcall sig svos sargs
-  | Bbuiltin ef args res pc _ =>
+  | Bbuiltin ef args res pc =>
     let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in
     Sbuiltin ef sargs res pc
-  | Breturn or _ => 
+  | Breturn or => 
     let sor := SOME r <- or IN Some (sis.(si_sreg) r) in
     Sreturn sor
-  | Bjumptable reg tbl _ =>
+  | Bjumptable reg tbl =>
     let sv := sis.(si_sreg) reg in
     Sjumptable sv tbl
   end.
@@ -770,7 +770,7 @@ pour représenter l'ensemble des chemins.
 
 Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := 
   match ib with
-  | BF fin => Sfinal sis (sexec_final_sfv fin sis)
+  | BF fin _ => Sfinal sis (sexec_final_sfv fin sis)
   (* basic instructions *)
   | Bnop _ => k sis
   | Bop op args res _ => k (sexec_op op args res sis)
@@ -780,7 +780,7 @@ Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate :=
  (* composed instructions *)
   | Bseq ib1 ib2 =>
       sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) 
-  | Bcond cond args ifso ifnot _ _ =>
+  | Bcond cond args ifso ifnot _ =>
       let args := list_sval_inj (List.map sis.(si_sreg) args) in
       let ifso := sexec_rec ifso sis k in
       let ifnot := sexec_rec ifnot sis k in