From 7703c4ca86a390303d0a120f8811c8fd704c5168 Mon Sep 17 00:00:00 2001
From: Sidney Congard
Date: Tue, 21 Jun 2022 11:41:09 +0200
Subject: concrete & symbolic evaluation work with new LLBC format

---
 src/ExtractToFStar.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'src/ExtractToFStar.ml')

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index b85c146b..b89579b5 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -6,7 +6,6 @@ open PureUtils
 open TranslateCore
 open PureToExtract
 open StringUtils
-open FunIdentifier
 module F = Format
 
 (** A qualifier for a type definition.
@@ -315,7 +314,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     fname ^ suffix
   in
 
-  let decreases_clause_name (_fid : FunDeclId.id) (fname : fun_name) : string =
+  let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string =
     let fname = fun_name_to_snake_case fname in
     (* Compute the suffix *)
     let suffix = "_decreases" in
-- 
cgit v1.2.3