diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml index 0f02e8203..63b14a3ec 100644 --- 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" ^ " " ^ "["