Fix

cryspen · Nov 21, 2023 · 2f14e68 · 2f14e68
1 parent bb5a757
commit 2f14e68
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml
@@ -1927,7 +1927,7 @@ struct
                                       ~f:(fun x -> plocal_ident x ^ "_loc")
                                       (match
                                          Map.find ctx.analysis_data.mut_var
-                                           x.ii_ident
+                                           (pconcrete_ident x.ii_ident)
                                        with
                                       | Some (l, _) -> l
                                       | _ -> []))
@@ -1949,7 +1949,7 @@ struct
                                     (pty span body.typ)
                                     (match
                                        Map.find ctx.analysis_data.mut_var
-                                         x.ii_ident
+                                         (pconcrete_ident x.ii_ident)
                                      with
                                     | Some (_ :: _, _) -> []
                                     | _ -> [ "fset []" ])
@@ -2014,7 +2014,7 @@ struct
                   SSP.AST.Value (SSP.AST.Literal (Int.to_string x_n), false);
                 ] ),
             SSP.AST.NameTy "Location" ))
-      (match Map.find ctx.analysis_data.mut_var name with
+      (match Map.find ctx.analysis_data.mut_var (pconcrete_ident name) with
       | Some l -> snd l
       | None -> [])
 
@@ -2051,7 +2051,7 @@ struct
 
   and both_return_type_from_name lis iis name typ (extra_L : string list) =
     let mvars_ext_L =
-      match Map.find ctx.analysis_data.mut_var name with
+      match Map.find ctx.analysis_data.mut_var (pconcrete_ident name) with
       | Some (l, l2) when List.length l > 0 ->
           [
             "fset" ^ " " ^ "["