chore(upgrade) Ergo compiler code switched to Coq 8.12

Signed-off-by: Jerome Simeon <jeromesimeon@me.com>
accordproject · Apr 5, 2021 · 28b9673 · 28b9673
1 parent 1100f51
commit 28b9673
Show file tree

Hide file tree

Showing 528 changed files with 29,231 additions and 118,524 deletions.
diff --git a/.Makefile.coq.d b/.Makefile.coq.d
diff --git a/.circleci/config.yml b/.circleci/config.yml
@@ -43,12 +43,12 @@ common_steps: &common_steps
     - run:
         name: "Install Coq"
         command: |
-          opam install -y -v coq.8.8.2 coq-flocq coq-jsast
+          opam install -y -v coq.8.12.0 coq-flocq coq-jsast
         no_output_timeout: 30m
     - run:
         name: "Install Q*cert"
         command: |
-          opam install -y -v coq-qcert.2.0.0
+          opam install -y -v coq-qcert.2.1.0
         no_output_timeout: 30m
     - save_cache:
         <<: *common_cache_key

diff --git a/.gitignore b/.gitignore
@@ -18,9 +18,13 @@ Makefile.config
 *~
 .#*
 *.vo
+*.vos
+*.vok
 *.v.d
 *.glob
 *.aux
+*.lia.cache
+.Makefile.coq.d
 *.ctoj
 .DS_Store
 _CoqProject
@@ -48,4 +52,3 @@ thumbs.db
 # generated by dune
 *.merlin
 *.install
-
diff --git a/compiler/core/Backend/Component/DateTimeComponent.vok b/compiler/core/Backend/Component/DateTimeComponent.vok
diff --git a/compiler/core/Backend/Component/DateTimeComponent.vos b/compiler/core/Backend/Component/DateTimeComponent.vos
diff --git a/compiler/core/Backend/Component/LogComponent.vok b/compiler/core/Backend/Component/LogComponent.vok
diff --git a/compiler/core/Backend/Component/LogComponent.vos b/compiler/core/Backend/Component/LogComponent.vos
diff --git a/compiler/core/Backend/Component/MathComponent.vok b/compiler/core/Backend/Component/MathComponent.vok
diff --git a/compiler/core/Backend/Component/MathComponent.vos b/compiler/core/Backend/Component/MathComponent.vos
diff --git a/compiler/core/Backend/Component/MonetaryAmountComponent.vok b/compiler/core/Backend/Component/MonetaryAmountComponent.vok
diff --git a/compiler/core/Backend/Component/MonetaryAmountComponent.vos b/compiler/core/Backend/Component/MonetaryAmountComponent.vos
diff --git a/compiler/core/Backend/ForeignErgo.vok b/compiler/core/Backend/ForeignErgo.vok
diff --git a/compiler/core/Backend/ForeignErgo.vos b/compiler/core/Backend/ForeignErgo.vos
diff --git a/compiler/core/Backend/ForeignModel.vok b/compiler/core/Backend/ForeignModel.vok
diff --git a/compiler/core/Backend/ForeignModel.vos b/compiler/core/Backend/ForeignModel.vos
diff --git a/compiler/core/Backend/Lib/QBackendModel.vok b/compiler/core/Backend/Lib/QBackendModel.vok
diff --git a/compiler/core/Backend/Lib/QBackendModel.vos b/compiler/core/Backend/Lib/QBackendModel.vos
diff --git a/compiler/core/Backend/Lib/QBackendRuntime.vok b/compiler/core/Backend/Lib/QBackendRuntime.vok
diff --git a/compiler/core/Backend/Lib/QBackendRuntime.vos b/compiler/core/Backend/Lib/QBackendRuntime.vos
diff --git a/compiler/core/Backend/Lib/QCodeGen.vok b/compiler/core/Backend/Lib/QCodeGen.vok
diff --git a/compiler/core/Backend/Lib/QCodeGen.vos b/compiler/core/Backend/Lib/QCodeGen.vos
diff --git a/compiler/core/Backend/Lib/QData.vok b/compiler/core/Backend/Lib/QData.vok
diff --git a/compiler/core/Backend/Lib/QData.vos b/compiler/core/Backend/Lib/QData.vos
diff --git a/compiler/core/Backend/Lib/QOps.vok b/compiler/core/Backend/Lib/QOps.vok
diff --git a/compiler/core/Backend/Lib/QOps.vos b/compiler/core/Backend/Lib/QOps.vos
diff --git a/compiler/core/Backend/Lib/QType.vok b/compiler/core/Backend/Lib/QType.vok
diff --git a/compiler/core/Backend/Lib/QType.vos b/compiler/core/Backend/Lib/QType.vos
diff --git a/compiler/core/Backend/QLib.vok b/compiler/core/Backend/QLib.vok
diff --git a/compiler/core/Backend/QLib.vos b/compiler/core/Backend/QLib.vos
diff --git a/compiler/core/Backend/Qcert/QcertCompiler.vok b/compiler/core/Backend/Qcert/QcertCompiler.vok
diff --git a/compiler/core/Backend/Qcert/QcertCompiler.vos b/compiler/core/Backend/Qcert/QcertCompiler.vos
diff --git a/compiler/core/Backend/Qcert/QcertData.v b/compiler/core/Backend/Qcert/QcertData.v
@@ -109,7 +109,7 @@ Definition onddateTime {A} (f : DATE_TIME -> A) (d : data) : option A :=
 
 Definition lift_dateTimeList (l:list data) : option (list DATE_TIME) :=
   lift_map
-    (fun d =>
+    (fun d : data =>
        match d with
        | dforeign (enhanceddateTime fd) => Some fd
        | _ => None
@@ -512,7 +512,6 @@ Next Obligation.
   - destruct m; simpl in H;
       unfold ondfloat2, lift in H
       ; destruct d1; simpl in H; try discriminate
-      ; destruct f; simpl in H; try discriminate
       ; destruct d2; simpl in H; try discriminate
       ; try (destruct f; simpl in H; try discriminate)
       ; invcs H

diff --git a/compiler/core/Backend/Qcert/QcertData.vok b/compiler/core/Backend/Qcert/QcertData.vok
diff --git a/compiler/core/Backend/Qcert/QcertData.vos b/compiler/core/Backend/Qcert/QcertData.vos
diff --git a/compiler/core/Backend/Qcert/QcertDataToEJson.vok b/compiler/core/Backend/Qcert/QcertDataToEJson.vok
diff --git a/compiler/core/Backend/Qcert/QcertDataToEJson.vos b/compiler/core/Backend/Qcert/QcertDataToEJson.vos
diff --git a/compiler/core/Backend/Qcert/QcertDataTyping.vok b/compiler/core/Backend/Qcert/QcertDataTyping.vok
diff --git a/compiler/core/Backend/Qcert/QcertDataTyping.vos b/compiler/core/Backend/Qcert/QcertDataTyping.vos
diff --git a/compiler/core/Backend/Qcert/QcertEJson.v b/compiler/core/Backend/Qcert/QcertEJson.v
@@ -413,7 +413,7 @@ Definition enhanced_ejson_date_time_runtime_op_interp op (dl:list ejson) : optio
          end) dl
   | EJsonRuntimeDateTimeDurationAmount =>
     apply_unary
-      (fun d =>
+      (fun d : ejson =>
          match d with
          | ejforeign (enhanceddateTimeduration fd) =>
            Some (ejbigint (DATE_TIME_DURATION_amount fd))

diff --git a/compiler/core/Backend/Qcert/QcertEJson.vok b/compiler/core/Backend/Qcert/QcertEJson.vok
diff --git a/compiler/core/Backend/Qcert/QcertEJson.vos b/compiler/core/Backend/Qcert/QcertEJson.vos
diff --git a/compiler/core/Backend/Qcert/QcertEJsonToJSON.vok b/compiler/core/Backend/Qcert/QcertEJsonToJSON.vok
diff --git a/compiler/core/Backend/Qcert/QcertEJsonToJSON.vos b/compiler/core/Backend/Qcert/QcertEJsonToJSON.vos
diff --git a/compiler/core/Backend/Qcert/QcertModel.vok b/compiler/core/Backend/Qcert/QcertModel.vok
diff --git a/compiler/core/Backend/Qcert/QcertModel.vos b/compiler/core/Backend/Qcert/QcertModel.vos
diff --git a/compiler/core/Backend/Qcert/QcertReduceOps.vok b/compiler/core/Backend/Qcert/QcertReduceOps.vok
diff --git a/compiler/core/Backend/Qcert/QcertReduceOps.vos b/compiler/core/Backend/Qcert/QcertReduceOps.vos
diff --git a/compiler/core/Backend/Qcert/QcertRuntime.vok b/compiler/core/Backend/Qcert/QcertRuntime.vok
diff --git a/compiler/core/Backend/Qcert/QcertRuntime.vos b/compiler/core/Backend/Qcert/QcertRuntime.vos
diff --git a/compiler/core/Backend/Qcert/QcertToJava.vok b/compiler/core/Backend/Qcert/QcertToJava.vok
diff --git a/compiler/core/Backend/Qcert/QcertToJava.vos b/compiler/core/Backend/Qcert/QcertToJava.vos
diff --git a/compiler/core/Backend/Qcert/QcertToJavascriptAst.vok b/compiler/core/Backend/Qcert/QcertToJavascriptAst.vok
diff --git a/compiler/core/Backend/Qcert/QcertToJavascriptAst.vos b/compiler/core/Backend/Qcert/QcertToJavascriptAst.vos
diff --git a/compiler/core/Backend/Qcert/QcertToReduceOps.vok b/compiler/core/Backend/Qcert/QcertToReduceOps.vok
diff --git a/compiler/core/Backend/Qcert/QcertToReduceOps.vos b/compiler/core/Backend/Qcert/QcertToReduceOps.vos
diff --git a/compiler/core/Backend/Qcert/QcertToScala.vok b/compiler/core/Backend/Qcert/QcertToScala.vok
diff --git a/compiler/core/Backend/Qcert/QcertToScala.vos b/compiler/core/Backend/Qcert/QcertToScala.vos
diff --git a/compiler/core/Backend/Qcert/QcertToSpark.vok b/compiler/core/Backend/Qcert/QcertToSpark.vok
diff --git a/compiler/core/Backend/Qcert/QcertToSpark.vos b/compiler/core/Backend/Qcert/QcertToSpark.vos
diff --git a/compiler/core/Backend/Qcert/QcertType.v b/compiler/core/Backend/Qcert/QcertType.v
@@ -111,7 +111,7 @@ Proof.
     inversion H; inversion H0; congruence.
 Qed.
 
-Instance enhanced_type_lattice : Lattice enhanced_type eq
+#[refine] Instance enhanced_type_lattice : Lattice enhanced_type eq
   := {
       join := enhanced_type_join
       ; meet := enhanced_type_meet

diff --git a/compiler/core/Backend/Qcert/QcertType.vok b/compiler/core/Backend/Qcert/QcertType.vok
diff --git a/compiler/core/Backend/Qcert/QcertType.vos b/compiler/core/Backend/Qcert/QcertType.vos
diff --git a/compiler/core/Backend/Qcert/QcertTypeToJSON.vok b/compiler/core/Backend/Qcert/QcertTypeToJSON.vok
diff --git a/compiler/core/Backend/Qcert/QcertTypeToJSON.vos b/compiler/core/Backend/Qcert/QcertTypeToJSON.vos
diff --git a/compiler/core/Backend/Qcert/QcertTyping.vok b/compiler/core/Backend/Qcert/QcertTyping.vok
diff --git a/compiler/core/Backend/Qcert/QcertTyping.vos b/compiler/core/Backend/Qcert/QcertTyping.vos
diff --git a/compiler/core/Common/Ast.vok b/compiler/core/Common/Ast.vok
diff --git a/compiler/core/Common/Ast.vos b/compiler/core/Common/Ast.vos
diff --git a/compiler/core/Common/Names.vok b/compiler/core/Common/Names.vok
diff --git a/compiler/core/Common/Names.vos b/compiler/core/Common/Names.vos
diff --git a/compiler/core/Common/NamespaceContext.vok b/compiler/core/Common/NamespaceContext.vok
diff --git a/compiler/core/Common/NamespaceContext.vos b/compiler/core/Common/NamespaceContext.vos
diff --git a/compiler/core/Common/PrintTypedData.v b/compiler/core/Common/PrintTypedData.v
@@ -62,7 +62,7 @@ Section PrintTypedData.
       | _ => None
       end.
 
-    Definition fmt_nl := String.String (ascii_of_N 10) EmptyString.
+    Definition fmt_nl := String.String (ascii_of_nat 10) EmptyString.
     Definition fmt_dq := """".
 
     Definition js_quote_char (a:ascii) : string

diff --git a/compiler/core/Common/PrintTypedData.vok b/compiler/core/Common/PrintTypedData.vok
diff --git a/compiler/core/Common/PrintTypedData.vos b/compiler/core/Common/PrintTypedData.vos
diff --git a/compiler/core/Common/Provenance.vok b/compiler/core/Common/Provenance.vok
diff --git a/compiler/core/Common/Provenance.vos b/compiler/core/Common/Provenance.vos
diff --git a/compiler/core/Common/Result.vok b/compiler/core/Common/Result.vok
diff --git a/compiler/core/Common/Result.vos b/compiler/core/Common/Result.vos
diff --git a/compiler/core/Compiler/ErgoCompiler.v b/compiler/core/Compiler/ErgoCompiler.v
@@ -12,8 +12,9 @@
  * limitations under the License.
  *)
 
-Require String.
-Require Qcert.Brands.BrandRelation.
+Require Import String.
+Require Import ZArith.
+Require Import Qcert.Brands.BrandRelation.
 
 Require ErgoSpec.Version.
 Require ErgoSpec.Utils.Misc.

diff --git a/compiler/core/Compiler/ErgoCompiler.vok b/compiler/core/Compiler/ErgoCompiler.vok
diff --git a/compiler/core/Compiler/ErgoCompiler.vos b/compiler/core/Compiler/ErgoCompiler.vos
diff --git a/compiler/core/Compiler/ErgoDriver.vok b/compiler/core/Compiler/ErgoDriver.vok
diff --git a/compiler/core/Compiler/ErgoDriver.vos b/compiler/core/Compiler/ErgoDriver.vos
diff --git a/compiler/core/Ergo/Lang/Ergo.vok b/compiler/core/Ergo/Lang/Ergo.vok
diff --git a/compiler/core/Ergo/Lang/Ergo.vos b/compiler/core/Ergo/Lang/Ergo.vos
diff --git a/compiler/core/Ergo/Lang/ErgoMap.vok b/compiler/core/Ergo/Lang/ErgoMap.vok
diff --git a/compiler/core/Ergo/Lang/ErgoMap.vos b/compiler/core/Ergo/Lang/ErgoMap.vos
diff --git a/compiler/core/Ergo/Lang/ErgoSem.vok b/compiler/core/Ergo/Lang/ErgoSem.vok
diff --git a/compiler/core/Ergo/Lang/ErgoSem.vos b/compiler/core/Ergo/Lang/ErgoSem.vos
diff --git a/compiler/core/Ergo/Lang/ErgoSugar.vok b/compiler/core/Ergo/Lang/ErgoSugar.vok
diff --git a/compiler/core/Ergo/Lang/ErgoSugar.vos b/compiler/core/Ergo/Lang/ErgoSugar.vos
diff --git a/compiler/core/ErgoC/Lang/ErgoC.vok b/compiler/core/ErgoC/Lang/ErgoC.vok
diff --git a/compiler/core/ErgoC/Lang/ErgoC.vos b/compiler/core/ErgoC/Lang/ErgoC.vos
diff --git a/compiler/core/ErgoC/Lang/ErgoCEval.vok b/compiler/core/ErgoC/Lang/ErgoCEval.vok
diff --git a/compiler/core/ErgoC/Lang/ErgoCEval.vos b/compiler/core/ErgoC/Lang/ErgoCEval.vos
diff --git a/compiler/core/ErgoC/Lang/ErgoCEvalContext.vok b/compiler/core/ErgoC/Lang/ErgoCEvalContext.vok
diff --git a/compiler/core/ErgoC/Lang/ErgoCEvalContext.vos b/compiler/core/ErgoC/Lang/ErgoCEvalContext.vos
diff --git a/compiler/core/ErgoC/Lang/ErgoCExpand.vok b/compiler/core/ErgoC/Lang/ErgoCExpand.vok
diff --git a/compiler/core/ErgoC/Lang/ErgoCExpand.vos b/compiler/core/ErgoC/Lang/ErgoCExpand.vos
diff --git a/compiler/core/ErgoC/Lang/ErgoCOverloaded.v b/compiler/core/ErgoC/Lang/ErgoCOverloaded.v
@@ -14,6 +14,7 @@
 
 Require Import String.
 Require Import List.
+Require Import ZArith.
 Require Import Basics.
 
 Require Import ErgoSpec.Utils.Misc.

diff --git a/compiler/core/ErgoC/Lang/ErgoCOverloaded.vok b/compiler/core/ErgoC/Lang/ErgoCOverloaded.vok
diff --git a/compiler/core/ErgoC/Lang/ErgoCOverloaded.vos b/compiler/core/ErgoC/Lang/ErgoCOverloaded.vos
diff --git a/compiler/core/ErgoC/Lang/ErgoCStdlib.vok b/compiler/core/ErgoC/Lang/ErgoCStdlib.vok
diff --git a/compiler/core/ErgoC/Lang/ErgoCStdlib.vos b/compiler/core/ErgoC/Lang/ErgoCStdlib.vos
diff --git a/compiler/core/ErgoC/Lang/ErgoCSugar.vok b/compiler/core/ErgoC/Lang/ErgoCSugar.vok
diff --git a/compiler/core/ErgoC/Lang/ErgoCSugar.vos b/compiler/core/ErgoC/Lang/ErgoCSugar.vos
diff --git a/compiler/core/ErgoC/Lang/ErgoCT.vok b/compiler/core/ErgoC/Lang/ErgoCT.vok
diff --git a/compiler/core/ErgoC/Lang/ErgoCT.vos b/compiler/core/ErgoC/Lang/ErgoCT.vos
diff --git a/compiler/core/ErgoC/Lang/ErgoCTypecheck.vok b/compiler/core/ErgoC/Lang/ErgoCTypecheck.vok
diff --git a/compiler/core/ErgoC/Lang/ErgoCTypecheck.vos b/compiler/core/ErgoC/Lang/ErgoCTypecheck.vos
diff --git a/compiler/core/ErgoC/Lang/ErgoCTypecheckContext.vok b/compiler/core/ErgoC/Lang/ErgoCTypecheckContext.vok
diff --git a/compiler/core/ErgoC/Lang/ErgoCTypecheckContext.vos b/compiler/core/ErgoC/Lang/ErgoCTypecheckContext.vos
diff --git a/compiler/core/ErgoImp/Lang/ErgoImp.vok b/compiler/core/ErgoImp/Lang/ErgoImp.vok
diff --git a/compiler/core/ErgoImp/Lang/ErgoImp.vos b/compiler/core/ErgoImp/Lang/ErgoImp.vos
diff --git a/compiler/core/ErgoNNRC/Lang/ErgoNNRC.vok b/compiler/core/ErgoNNRC/Lang/ErgoNNRC.vok
diff --git a/compiler/core/ErgoNNRC/Lang/ErgoNNRC.vos b/compiler/core/ErgoNNRC/Lang/ErgoNNRC.vos
diff --git a/compiler/core/ErgoNNRC/Lang/ErgoNNRCSugar.v b/compiler/core/ErgoNNRC/Lang/ErgoNNRCSugar.v
@@ -18,6 +18,7 @@
 
 Require Import String.
 Require Import List.
+Require Import ZArith.
 Require Import Qcert.NNRC.NNRCRuntime.
 Require Import ErgoSpec.Common.Names.
 Require Import ErgoSpec.ErgoNNRC.Lang.ErgoNNRC.

diff --git a/compiler/core/ErgoNNRC/Lang/ErgoNNRCSugar.vok b/compiler/core/ErgoNNRC/Lang/ErgoNNRCSugar.vok
diff --git a/compiler/core/ErgoNNRC/Lang/ErgoNNRCSugar.vos b/compiler/core/ErgoNNRC/Lang/ErgoNNRCSugar.vos
diff --git a/compiler/core/Tests/HelloWorld.vok b/compiler/core/Tests/HelloWorld.vok
diff --git a/compiler/core/Tests/HelloWorld.vos b/compiler/core/Tests/HelloWorld.vos
diff --git a/compiler/core/Translation/CTOtoErgo.vok b/compiler/core/Translation/CTOtoErgo.vok
diff --git a/compiler/core/Translation/CTOtoErgo.vos b/compiler/core/Translation/CTOtoErgo.vos
diff --git a/compiler/core/Translation/ErgoAssembly.v b/compiler/core/Translation/ErgoAssembly.v
@@ -41,7 +41,7 @@ Section ErgoAssembly.
                                "org.accordproject.ergo.stdlib.toText"%string
                                (template::nil)))).
 
-  Fixpoint add_template_to_clauses (prov:provenance) (template:list (string * laergo_expr)) (cl:list laergo_clause) :=
+  Definition add_template_to_clauses (prov:provenance) (template:list (string * laergo_expr)) (cl:list laergo_clause) :=
     cl ++ (List.map (fun xy => toDraftClause prov (fst xy) (snd xy)) template).
 
   Definition add_template_to_contract (template:list (string * laergo_expr)) (c:laergo_contract) :=

diff --git a/compiler/core/Translation/ErgoAssembly.vok b/compiler/core/Translation/ErgoAssembly.vok
diff --git a/compiler/core/Translation/ErgoAssembly.vos b/compiler/core/Translation/ErgoAssembly.vos
diff --git a/compiler/core/Translation/ErgoCInline.vok b/compiler/core/Translation/ErgoCInline.vok
diff --git a/compiler/core/Translation/ErgoCInline.vos b/compiler/core/Translation/ErgoCInline.vos
diff --git a/compiler/core/Translation/ErgoCTtoErgoNNRC.v b/compiler/core/Translation/ErgoCTtoErgoNNRC.v
@@ -16,6 +16,7 @@
 
 Require Import String.
 Require Import List.
+Require Import ZArith.
 
 Require Import Qcert.NNRC.NNRCRuntime.
 

diff --git a/compiler/core/Translation/ErgoCTtoErgoNNRC.vok b/compiler/core/Translation/ErgoCTtoErgoNNRC.vok
diff --git a/compiler/core/Translation/ErgoCTtoErgoNNRC.vos b/compiler/core/Translation/ErgoCTtoErgoNNRC.vos
diff --git a/compiler/core/Translation/ErgoCompContext.vok b/compiler/core/Translation/ErgoCompContext.vok
diff --git a/compiler/core/Translation/ErgoCompContext.vos b/compiler/core/Translation/ErgoCompContext.vos
diff --git a/compiler/core/Translation/ErgoImptoES6.vok b/compiler/core/Translation/ErgoImptoES6.vok
diff --git a/compiler/core/Translation/ErgoImptoES6.vos b/compiler/core/Translation/ErgoImptoES6.vos
diff --git a/compiler/core/Translation/ErgoNNRCtoErgoImp.vok b/compiler/core/Translation/ErgoNNRCtoErgoImp.vok
diff --git a/compiler/core/Translation/ErgoNNRCtoErgoImp.vos b/compiler/core/Translation/ErgoNNRCtoErgoImp.vos
diff --git a/compiler/core/Translation/ErgoNNRCtoJava.vok b/compiler/core/Translation/ErgoNNRCtoJava.vok
diff --git a/compiler/core/Translation/ErgoNNRCtoJava.vos b/compiler/core/Translation/ErgoNNRCtoJava.vos
diff --git a/compiler/core/Translation/ErgoNameResolve.vok b/compiler/core/Translation/ErgoNameResolve.vok
diff --git a/compiler/core/Translation/ErgoNameResolve.vos b/compiler/core/Translation/ErgoNameResolve.vos
diff --git a/compiler/core/Translation/ErgotoErgoC.vok b/compiler/core/Translation/ErgotoErgoC.vok
diff --git a/compiler/core/Translation/ErgotoErgoC.vos b/compiler/core/Translation/ErgotoErgoC.vos
diff --git a/compiler/core/Types/CTO.vok b/compiler/core/Types/CTO.vok
diff --git a/compiler/core/Types/CTO.vos b/compiler/core/Types/CTO.vos
diff --git a/compiler/core/Types/ErgoType.vok b/compiler/core/Types/ErgoType.vok
diff --git a/compiler/core/Types/ErgoType.vos b/compiler/core/Types/ErgoType.vos
diff --git a/compiler/core/Types/ErgoTypetoQcertType.v b/compiler/core/Types/ErgoTypetoQcertType.v
@@ -92,7 +92,7 @@ Section ErgoTypetoQcertType.
       | ErgoTypeContract _ _ _ => ctxt
       end.
 
-    Fixpoint ergo_expand_extends_in_declarations (decls:list laergo_type_declaration) : expand_ctxt :=
+    Definition ergo_expand_extends_in_declarations (decls:list laergo_type_declaration) : expand_ctxt :=
       List.fold_left
         (fun ctxt decl =>
            ergo_decl_expand_extends

diff --git a/compiler/core/Types/ErgoTypetoQcertType.vok b/compiler/core/Types/ErgoTypetoQcertType.vok
diff --git a/compiler/core/Types/ErgoTypetoQcertType.vos b/compiler/core/Types/ErgoTypetoQcertType.vos
diff --git a/compiler/core/Types/QcertTypeUtil.vok b/compiler/core/Types/QcertTypeUtil.vok
diff --git a/compiler/core/Types/QcertTypeUtil.vos b/compiler/core/Types/QcertTypeUtil.vos
diff --git a/compiler/core/Utils/Misc.v b/compiler/core/Utils/Misc.v
@@ -49,7 +49,7 @@ Section Misc.
     Definition postpend {A} (ls : list A) (a : A) : list A :=
       ls ++ (a :: nil).
 
-    Fixpoint last_some {A} (l:list (option A)) : option A :=
+    Definition last_some {A} (l:list (option A)) : option A :=
       let proc_one (one:option A) (acc:option A) :=
           match acc with
           | Some x => Some x
@@ -61,7 +61,7 @@ Section Misc.
         None
         l.
 
-    Fixpoint last_some_pair {A} {B} (l:list ((option A) * (option B))) : ((option A) * (option B)) :=
+    Definition last_some_pair {A} {B} (l:list ((option A) * (option B))) : ((option A) * (option B)) :=
       let proc_one (one : ((option A) * (option B))) (acc : ((option A) * (option B))) :=
           match acc with
           | (Some x, Some y) => acc

diff --git a/compiler/core/Utils/Misc.vok b/compiler/core/Utils/Misc.vok
diff --git a/compiler/core/Utils/Misc.vos b/compiler/core/Utils/Misc.vos
diff --git a/compiler/core/Version.vok b/compiler/core/Version.vok
diff --git a/compiler/core/Version.vos b/compiler/core/Version.vos
diff --git a/compiler/extraction/Apply.ml b/compiler/extraction/Apply.ml
diff --git a/compiler/extraction/Apply.mli b/compiler/extraction/Apply.mli
diff --git a/compiler/extraction/Ascii.ml b/compiler/extraction/Ascii.ml
diff --git a/compiler/extraction/Ascii.mli b/compiler/extraction/Ascii.mli
diff --git a/compiler/extraction/Assoc.ml b/compiler/extraction/Assoc.ml
diff --git a/compiler/extraction/Assoc.mli b/compiler/extraction/Assoc.mli