And on function nodes too

FStarLang · Oct 21, 2016 · b4ad801 · b4ad801
1 parent 524e14a
commit b4ad801
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/src/extraction/kremlin.fs b/src/extraction/kremlin.fs
@@ -33,7 +33,7 @@ type program =
 
 and decl =
   | DGlobal of list<flag> * lident * typ * expr
-  | DFunction of list<flag> * typ * lident * list<binder> * expr
+  | DFunction of option<cc> * list<flag> * typ * lident * list<binder> * expr
   | DTypeAlias of lident * int * typ
   | DTypeFlat of lident * fields_t
   | DExternal of option<cc> * lident * typ
@@ -347,10 +347,10 @@ and translate_decl env d: option<decl> =
       else begin
         try
           let body = translate_expr env body in
-          Some (DFunction (flags, t, name, binders, body))
+          Some (DFunction (None, flags, t, name, binders, body))
         with e ->
           Util.print2 "Warning: writing a stub for %s (%s)\n" (snd name) (Util.print_exn e);
-          Some (DFunction (flags, t, name, binders, EAbort))
+          Some (DFunction (None, flags, t, name, binders, EAbort))
       end
 
   | MLM_Let (flavor, flags, [ {

diff --git a/src/ocaml-output/FStar_Extraction_Kremlin.ml b/src/ocaml-output/FStar_Extraction_Kremlin.ml
@@ -3,7 +3,7 @@ open Prims
 
 type decl =
 | DGlobal of (flag Prims.list * lident * typ * expr)
-| DFunction of (flag Prims.list * typ * lident * binder Prims.list * expr)
+| DFunction of (cc Prims.option * flag Prims.list * typ * lident * binder Prims.list * expr)
 | DTypeAlias of (lident * Prims.int * typ)
 | DTypeFlat of (lident * fields_t)
 | DExternal of (cc Prims.option * lident * typ)
@@ -1545,15 +1545,15 @@ try
 (
 
 let body = (translate_expr env body)
-in Some (DFunction (((flags), (t), (name), (binders), (body)))))
+in Some (DFunction (((None), (flags), (t), (name), (binders), (body)))))
 end)
 with
 | e -> begin
 (
 
 let _81_401 = (let _175_766 = (FStar_Util.print_exn e)
 in (FStar_Util.print2 "Warning: writing a stub for %s (%s)\n" (Prims.snd name) _175_766))
-in Some (DFunction (((flags), (t), (name), (binders), (EAbort)))))
+in Some (DFunction (((None), (flags), (t), (name), (binders), (EAbort)))))
 end
 end))))))))
 end