Fix deprecation and unnecessary module

MetaCoq · Mar 18, 2024 · 05cffdf · 05cffdf
1 parent 897faa1
commit 05cffdf
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/template-coq/gen-src/metacoq_template_plugin.mlpack b/template-coq/gen-src/metacoq_template_plugin.mlpack
@@ -118,7 +118,6 @@ TemplateProgram
 
 Wf
 NoConfusion
-MCUint63
 Init
 FloatClass
 DepElim

diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml
@@ -264,7 +264,7 @@ struct
 
   let cofixpoint_arities ts =
     let cofix_arity t =
-      let ctx, _concl = Term.decompose_prod_assum t in
+      let ctx, _concl = Term.decompose_prod_decls t in
       Context.Rel.nhyps ctx
     in Array.map cofix_arity ts
-Original file line number
+Diff line change
@@ Expand Up / @@ -118,7 +118,6 @@ TemplateProgram @@
     Wf
     NoConfusion
-    MCUint63
     Init
     FloatClass
     DepElim
@@ Expand Down @@