fix compilation

Author: yforster

pcuic/theories/PCUICToTemplateCorrectness.v

@@ -1427,7 +1427,7 @@ Proof.
 
     unfold decompose_app. simpl.
     rewrite PCUICAstUtils.atom_decompose_app. destruct t => /= //.
-    exists _, d2. split. lia.
+    eexists _, d2. split. lia.
     unshelve eexists.
     econstructor. exists s; eauto. reflexivity. assumption. constructor.
     simpl. lia.
@@ -1640,4 +1640,4 @@ Proof.
     + now eapply trans_cumul.
 Qed.
 
-Print Assumptions pcuic_to_template.
+Print Assumptions pcuic_to_template.

template-coq/gen-src/specFloat.ml.rej

@@ -1,16 +1,10 @@
-***************
-*** 4,9 ****
-  open Datatypes
-  open Zbool
-  open Zpower
-  
-  type spec_float =
-  | S754_zero of bool
---- 4,10 ----
-  open Datatypes
-  open Zbool
-  open Zpower
-+ open Float64
-  
-  type spec_float =
-  | S754_zero of bool
+--- gen-src/specFloat.ml.orig	2020-12-04 21:48:20.000000000 +0100
++++ gen-src/specFloat.ml	2020-12-04 21:48:33.000000000 +0100
+@@ -4,6 +4,7 @@
+ open Datatypes
+ open Zbool
+ open Zpower
++open Float64
+ 
+ type spec_float =
+ | S754_zero of bool

template-coq/src/ast_denoter.ml

@@ -129,7 +129,7 @@ struct
 
   let unquote_evar env evm n l = 
     let id = Evar.unsafe_of_int (unquote_int n) in
-    evm, mkEvar (id, Array.of_list l)
+    evm, mkEvar (id, l)
 
   let unquote_bool (q : quoted_bool) : bool = q
 

template-coq/src/constr_denoter.ml

@@ -147,7 +147,7 @@ struct
     else 
       let id = unquote_nat id in
       let ev = Evar.unsafe_of_int id in
-      evm, Constr.mkEvar (ev, Array.of_list args)
+      evm, Constr.mkEvar (ev, args)
 
   let unquote_relevance trm =
     if Constr.equal trm (Lazy.force tRelevant) then

template-coq/src/run_template_monad.ml

@@ -227,7 +227,6 @@ let unquote_one_inductive_entry env evm trm (* of type one_inductive_entry *) :
     | id::ar::cnames::ctms::[] ->
        let id = unquote_ident id in
        let evm, ar = denote_term env evm ar in
-       let template = unquote_bool template in
        let cnames = List.map unquote_ident (unquote_list cnames) in
        let evm, ctms = map_evm (denote_term env) evm (unquote_list ctms) in
        evm, { mind_entry_typename = id ;