From d1c77fc0c56f10e4d906e9451ecf79e471675638 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 21 Jul 2024 16:03:42 +0200 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530 --- .../theories/Bidirectional/BDStrengthening.v | 2 +- pcuic/theories/Syntax/PCUICDepth.v | 2 +- pcuic/theories/Syntax/PCUICInduction.v | 2 +- quotation/theories/ToPCUIC/Stdlib/Numbers.v | 2 +- .../theories/ToTemplate/Stdlib/Numbers.v | 2 +- safechecker-plugin/_PluginProject.in | 2 + safechecker-plugin/clean_extraction.sh | 3 + .../src/metacoq_safechecker_plugin.mlpack | 1 + safechecker-plugin/theories/Extraction.v | 2 + safechecker/theories/PCUICTypeChecker.v | 2 +- template-coq/Makefile | 7 --- template-coq/_PluginProject.in | 42 ++++++-------- .../gen-src/metacoq_template_plugin.mlpack | 6 ++ template-coq/gen-src/specFloat.ml.orig | 55 +++++++++++-------- template-coq/specFloat.patch | 4 +- template-coq/src/ast_denoter.ml | 2 +- template-coq/theories/Constants.v | 18 +++--- test-suite/safechecker_test.v | 3 +- utils/theories/bytestring.v | 4 +- 19 files changed, 86 insertions(+), 75 deletions(-) diff --git a/pcuic/theories/Bidirectional/BDStrengthening.v b/pcuic/theories/Bidirectional/BDStrengthening.v index baf715008..0d898be85 100644 --- a/pcuic/theories/Bidirectional/BDStrengthening.v +++ b/pcuic/theories/Bidirectional/BDStrengthening.v @@ -11,7 +11,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICGlobalEnv From MetaCoq.PCUIC Require Import BDTyping BDToPCUIC BDFromPCUIC. Require Import ssreflect ssrbool. -Require Import Coq.Program.Equality. +From Coq.Program Require Import Equality. Ltac case_inequalities := match goal with diff --git a/pcuic/theories/Syntax/PCUICDepth.v b/pcuic/theories/Syntax/PCUICDepth.v index 71a94c8b1..ede5c7f42 100644 --- a/pcuic/theories/Syntax/PCUICDepth.v +++ b/pcuic/theories/Syntax/PCUICDepth.v @@ -1,5 +1,5 @@ (* Distributed under the terms of the MIT license. *) -From Coq Require Import ssreflect Program Lia BinPos Arith.Compare_dec Bool. +From Coq Require Import ssreflect Program Lia BinPos Compare_dec Bool. From MetaCoq.Utils Require Import utils LibHypsNaming. From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases PCUICSize PCUICInduction. From Coq Require Import List. diff --git a/pcuic/theories/Syntax/PCUICInduction.v b/pcuic/theories/Syntax/PCUICInduction.v index 3c2676cab..23ffeb79d 100644 --- a/pcuic/theories/Syntax/PCUICInduction.v +++ b/pcuic/theories/Syntax/PCUICInduction.v @@ -1,5 +1,5 @@ (* Distributed under the terms of the MIT license. *) -From Coq Require Import ssreflect Program Lia BinPos Arith.Compare_dec Bool. +From Coq Require Import ssreflect Program Lia BinPos Compare_dec Bool. From MetaCoq.Utils Require Import utils LibHypsNaming. From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases PCUICSize. From Coq Require Import List. diff --git a/quotation/theories/ToPCUIC/Stdlib/Numbers.v b/quotation/theories/ToPCUIC/Stdlib/Numbers.v index 65c0e8ea4..1b674023d 100644 --- a/quotation/theories/ToPCUIC/Stdlib/Numbers.v +++ b/quotation/theories/ToPCUIC/Stdlib/Numbers.v @@ -2,7 +2,7 @@ From Coq.Numbers Require Import BinNums DecimalFacts HexadecimalFacts Cyclic.Int63.PrimInt63 Cyclic.Int63.Uint63 Cyclic.Abstract.CyclicAxioms Cyclic.Abstract.DoubleType - Cyclic.Abstract.CarryType + Cyclic.Int63.CarryType . From Coq Require Import ZArith. diff --git a/quotation/theories/ToTemplate/Stdlib/Numbers.v b/quotation/theories/ToTemplate/Stdlib/Numbers.v index 89fb4b9c6..f4473e30b 100644 --- a/quotation/theories/ToTemplate/Stdlib/Numbers.v +++ b/quotation/theories/ToTemplate/Stdlib/Numbers.v @@ -2,7 +2,7 @@ From Coq.Numbers Require Import BinNums DecimalFacts HexadecimalFacts Cyclic.Int63.PrimInt63 Cyclic.Int63.Uint63 Cyclic.Abstract.CyclicAxioms Cyclic.Abstract.DoubleType - Cyclic.Abstract.CarryType + Cyclic.Int63.CarryType . From Coq Require Import ZArith. From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init. diff --git a/safechecker-plugin/_PluginProject.in b/safechecker-plugin/_PluginProject.in index 5a2c45cb5..a7abaade4 100644 --- a/safechecker-plugin/_PluginProject.in +++ b/safechecker-plugin/_PluginProject.in @@ -13,6 +13,8 @@ src/uGraph0.ml src/uGraph0.mli src/wGraph.ml src/wGraph.mli +src/wf0.ml +src/wf0.mli # From PCUIC src/pCUICPrimitive.mli diff --git a/safechecker-plugin/clean_extraction.sh b/safechecker-plugin/clean_extraction.sh index 85e2f761a..772499c73 100755 --- a/safechecker-plugin/clean_extraction.sh +++ b/safechecker-plugin/clean_extraction.sh @@ -32,6 +32,9 @@ then # Remove extracted modules already linked in the template_coq plugin. echo "Removing:" $files rm -f $files + + # confusion between Init.Wf and Program.Wf + sed -i.bak src/pCUICSafeChecker.ml -e 's/open Wf/open Wf0/' else echo "Extraction up-to date" fi diff --git a/safechecker-plugin/src/metacoq_safechecker_plugin.mlpack b/safechecker-plugin/src/metacoq_safechecker_plugin.mlpack index 5557f37d6..0aafddedf 100644 --- a/safechecker-plugin/src/metacoq_safechecker_plugin.mlpack +++ b/safechecker-plugin/src/metacoq_safechecker_plugin.mlpack @@ -4,6 +4,7 @@ WGraph UGraph0 Reflect MCProd +Wf0 Classes0 Logic1 diff --git a/safechecker-plugin/theories/Extraction.v b/safechecker-plugin/theories/Extraction.v index 00a677373..ebe045a19 100644 --- a/safechecker-plugin/theories/Extraction.v +++ b/safechecker-plugin/theories/Extraction.v @@ -48,6 +48,8 @@ Next Obligation. eapply fake_abstract_guard_impl_properties. Qed. Definition infer_and_print_template_program_with_guard {cf} {nor} := @SafeTemplateChecker.infer_and_print_template_program cf nor fake_abstract_guard_impl. +From Stdlib.Program Require Import Wf. +Extraction Library Wf. Separate Extraction MakeOrderTac PCUICSafeChecker.typecheck_program infer_and_print_template_program_with_guard (* The following directives ensure separate extraction does not produce name clashes *) diff --git a/safechecker/theories/PCUICTypeChecker.v b/safechecker/theories/PCUICTypeChecker.v index 68cbe06d2..c2bd5d232 100644 --- a/safechecker/theories/PCUICTypeChecker.v +++ b/safechecker/theories/PCUICTypeChecker.v @@ -25,7 +25,7 @@ From MetaCoq.SafeChecker Require Import PCUICEqualityDec PCUICSafeReduce PCUICEr From Equations Require Import Equations. Require Import ssreflect ssrbool. -Require Import Stdlib.Program.Program. +From Stdlib Require Import Program. Local Set Keyed Unification. Set Equations Transparent. diff --git a/template-coq/Makefile b/template-coq/Makefile index c5c4d27ae..972ccdc11 100644 --- a/template-coq/Makefile +++ b/template-coq/Makefile @@ -74,14 +74,7 @@ cleanplugin: Makefile.plugin make -f Makefile.plugin clean PLUGIN_PROJECT_BLACKLIST := \ - carryType \ - coreTactics \ - depElim \ - floatClass \ - init \ mCUint63 \ - noConfusion \ - wf \ # space := $(subst ,, ) diff --git a/template-coq/_PluginProject.in b/template-coq/_PluginProject.in index abd10f638..f28ff7bb3 100644 --- a/template-coq/_PluginProject.in +++ b/template-coq/_PluginProject.in @@ -27,10 +27,6 @@ gen-src/binNums.ml gen-src/binNums.mli gen-src/binPos.ml gen-src/binPos.mli -gen-src/binPosDef.ml -gen-src/binPosDef.mli -gen-src/decidableClass.mli -gen-src/decidableClass.ml gen-src/bool.ml gen-src/bool.mli gen-src/byte.ml @@ -64,6 +60,8 @@ gen-src/coreTactics.ml gen-src/coreTactics.mli gen-src/datatypes.ml gen-src/datatypes.mli +gen-src/decidableClass.ml +gen-src/decidableClass.mli gen-src/decidableType.ml gen-src/decidableType.mli gen-src/decimal.ml @@ -101,20 +99,22 @@ gen-src/floatOps.ml gen-src/floatOps.mli gen-src/hexadecimal.ml gen-src/hexadecimal.mli -# gen-src/hexadecimalString.ml -# gen-src/hexadecimalString.mli gen-src/induction0.ml gen-src/induction0.mli gen-src/init.ml gen-src/init.mli gen-src/int0.ml gen-src/int0.mli +gen-src/intDef.ml +gen-src/intDef.mli gen-src/kernames.ml gen-src/kernames.mli gen-src/liftSubst.ml gen-src/liftSubst.mli gen-src/list0.ml gen-src/list0.mli +gen-src/listDef.ml +gen-src/listDef.mli gen-src/logic0.ml gen-src/logic0.mli gen-src/logic1.ml @@ -141,10 +141,6 @@ gen-src/mCRelations.ml gen-src/mCRelations.mli gen-src/mCString.ml gen-src/mCString.mli -gen-src/sint63.mli -gen-src/sint63.ml -gen-src/show.mli -gen-src/show.ml # gen-src/mCUint63.ml # gen-src/mCUint63.mli gen-src/mCUtils.ml @@ -165,6 +161,8 @@ gen-src/monad_utils.ml gen-src/monad_utils.mli gen-src/nat0.ml gen-src/nat0.mli +gen-src/natDef.ml +gen-src/natDef.mli gen-src/noConfusion.ml gen-src/noConfusion.mli gen-src/number.ml @@ -187,6 +185,8 @@ gen-src/peanoNat.ml gen-src/peanoNat.mli gen-src/plugin_core.ml gen-src/plugin_core.mli +gen-src/posDef.ml +gen-src/posDef.mli gen-src/pretty.ml gen-src/pretty.mli gen-src/primFloat.ml @@ -195,10 +195,10 @@ gen-src/primInt63.ml gen-src/primInt63.mli gen-src/primString.ml gen-src/primString.mli -gen-src/primitive.ml -gen-src/primitive.mli gen-src/primStringAxioms.ml gen-src/primStringAxioms.mli +gen-src/primitive.ml +gen-src/primitive.mli gen-src/quoter.ml gen-src/reflect.ml gen-src/reflect.mli @@ -209,16 +209,18 @@ gen-src/relation.ml gen-src/relation.mli gen-src/run_extractable.ml gen-src/run_extractable.mli +gen-src/show.ml +gen-src/show.mli gen-src/signature.ml gen-src/signature.mli +gen-src/sint63Axioms.ml +gen-src/sint63Axioms.mli gen-src/specFloat.ml gen-src/specFloat.mli gen-src/specif.ml gen-src/specif.mli gen-src/string0.ml gen-src/string0.mli -gen-src/sumbool.ml -gen-src/sumbool.mli gen-src/templateEnvMap.ml gen-src/templateEnvMap.mli gen-src/templateProgram.ml @@ -230,20 +232,12 @@ gen-src/transform.ml gen-src/transform.mli gen-src/typing0.ml gen-src/typing0.mli -gen-src/uint0.ml -gen-src/uint0.mli +gen-src/uint63Axioms.ml +gen-src/uint63Axioms.mli gen-src/universes0.ml gen-src/universes0.mli gen-src/wf.ml gen-src/wf.mli -gen-src/zArith_dec.ml -gen-src/zArith_dec.mli -gen-src/zbool.ml -gen-src/zbool.mli -gen-src/zeven.ml -gen-src/zeven.mli -gen-src/zpower.ml -gen-src/zpower.mli gen-src/metacoq_template_plugin.mlpack diff --git a/template-coq/gen-src/metacoq_template_plugin.mlpack b/template-coq/gen-src/metacoq_template_plugin.mlpack index 43f9a253d..394134ce8 100644 --- a/template-coq/gen-src/metacoq_template_plugin.mlpack +++ b/template-coq/gen-src/metacoq_template_plugin.mlpack @@ -7,6 +7,7 @@ Hexadecimal Numeral0 Nat0 Caml_nat +ListDef List0 PeanoNat Specif @@ -14,9 +15,13 @@ Basics BinPosDef BinNums BinPos +PosDef BinNat +NatDef BinInt +IntDef PrimInt63 +Uint63Axioms Uint0 Int63 Byte @@ -77,6 +82,7 @@ FloatOps PrimString PrimStringAxioms MCString +Sint63Axioms Sint63 Show MCUtils diff --git a/template-coq/gen-src/specFloat.ml.orig b/template-coq/gen-src/specFloat.ml.orig index 612fa74ed..010415afd 100644 --- a/template-coq/gen-src/specFloat.ml.orig +++ b/template-coq/gen-src/specFloat.ml.orig @@ -1,10 +1,7 @@ -open BinInt open BinNums -open BinPos -open Bool open Datatypes -open Zbool -open Zpower +open IntDef +open PosDef type spec_float = | S754_zero of bool @@ -39,7 +36,7 @@ let coq_Zdigits2 n = match n with (** val canonical_mantissa : coq_Z -> coq_Z -> positive -> coq_Z -> bool **) let canonical_mantissa prec emax m e = - coq_Zeq_bool (fexp prec emax (Z.add (Zpos (digits2_pos m)) e)) e + Z.eqb (fexp prec emax (Z.add (Zpos (digits2_pos m)) e)) e (** val bounded : coq_Z -> coq_Z -> positive -> coq_Z -> bool **) @@ -174,7 +171,7 @@ let binary_round_aux prec emax sx mx ex lx = let shl_align mx ex ex' = match Z.sub ex' ex with - | Zneg d -> ((shift_pos d mx), ex') + | Zneg d -> ((Pos.iter (fun x -> Coq_xO x) mx d), ex') | _ -> (mx, ex) (** val binary_round : @@ -283,8 +280,8 @@ let coq_SFclassify prec = function | S754_nan -> NaN | S754_finite (s, m, _) -> if s - then if Pos.eqb (digits2_pos m) (Z.to_pos prec) then NNormal else NSubn - else if Pos.eqb (digits2_pos m) (Z.to_pos prec) then PNormal else PSubn + then if Z.eqb (Zpos (digits2_pos m)) prec then NNormal else NSubn + else if Z.eqb (Zpos (digits2_pos m)) prec then PNormal else PSubn (** val coq_SFmul : coq_Z -> coq_Z -> spec_float -> spec_float -> spec_float **) @@ -323,12 +320,16 @@ let coq_SFadd prec emax x y = match x with | S754_zero sx -> (match y with - | S754_zero sy -> if eqb sx sy then x else S754_zero false + | S754_zero sy -> + if sx + then if sy then x else S754_zero false + else if sy then S754_zero false else x | S754_nan -> S754_nan | _ -> y) | S754_infinity sx -> (match y with - | S754_infinity sy -> if eqb sx sy then x else S754_nan + | S754_infinity sy -> + if sx then if sy then x else S754_nan else if sy then S754_nan else x | S754_nan -> S754_nan | _ -> x) | S754_nan -> S754_nan @@ -341,7 +342,8 @@ let coq_SFadd prec emax x y = let ez = Z.min ex ey in binary_normalize prec emax (Z.add (cond_Zopp sx (Zpos (fst (shl_align mx ex ez)))) - (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))) ez false) + (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))) + ez false) (** val coq_SFsub : coq_Z -> coq_Z -> spec_float -> spec_float -> spec_float **) @@ -350,13 +352,17 @@ let coq_SFsub prec emax x y = match x with | S754_zero sx -> (match y with - | S754_zero sy -> if eqb sx (negb sy) then x else S754_zero false + | S754_zero sy -> + if sx + then if sy then S754_zero false else x + else if sy then x else S754_zero false | S754_infinity sy -> S754_infinity (negb sy) | S754_nan -> S754_nan | S754_finite (sy, my, ey) -> S754_finite ((negb sy), my, ey)) | S754_infinity sx -> (match y with - | S754_infinity sy -> if eqb sx (negb sy) then x else S754_nan + | S754_infinity sy -> + if sx then if sy then S754_nan else x else if sy then x else S754_nan | S754_nan -> S754_nan | _ -> x) | S754_nan -> S754_nan @@ -369,19 +375,20 @@ let coq_SFsub prec emax x y = let ez = Z.min ex ey in binary_normalize prec emax (Z.sub (cond_Zopp sx (Zpos (fst (shl_align mx ex ez)))) - (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))) ez false) + (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))) + ez false) (** val new_location_even : coq_Z -> coq_Z -> location **) let new_location_even nb_steps k = - if coq_Zeq_bool k Z0 + if Z.eqb k Z0 then Coq_loc_Exact else Coq_loc_Inexact (Z.compare (Z.mul (Zpos (Coq_xO Coq_xH)) k) nb_steps) (** val new_location_odd : coq_Z -> coq_Z -> location **) let new_location_odd nb_steps k = - if coq_Zeq_bool k Z0 + if Z.eqb k Z0 then Coq_loc_Exact else Coq_loc_Inexact (match Z.compare @@ -456,7 +463,7 @@ let coq_SFsqrt_core_binary prec emax m e = | Zneg _ -> Z0 in let (q, r) = Z.sqrtrem m' in let l = - if coq_Zeq_bool r Z0 + if Z.eqb r Z0 then Coq_loc_Exact else Coq_loc_Inexact (if Z.leb r q then Lt else Gt) in @@ -491,11 +498,11 @@ let coq_SFldexp prec emax f e = let coq_SFfrexp prec emax f = match f with | S754_finite (sx, mx, ex) -> - if Pos.leb (Z.to_pos prec) (digits2_pos mx) + if Z.leb prec (Zpos (digits2_pos mx)) then ((S754_finite (sx, mx, (Z.opp prec))), (Z.add ex prec)) else let d = Z.sub prec (Zpos (digits2_pos mx)) in - ((S754_finite (sx, (shift_pos (Z.to_pos d) mx), (Z.opp prec))), - (Z.sub (Z.add ex prec) d)) + ((S754_finite (sx, (Pos.iter (fun x -> Coq_xO x) mx (Z.to_pos d)), + (Z.opp prec))), (Z.sub (Z.add ex prec) d)) | _ -> (f, (Z.sub (Z.mul (Zneg (Coq_xO Coq_xH)) emax) prec)) (** val coq_SFone : coq_Z -> coq_Z -> spec_float **) @@ -514,7 +521,8 @@ let coq_SFulp prec emax x = let coq_SFpred_pos prec emax x = match x with | S754_finite (_, mx, _) -> let d = - if Pos.eqb (Coq_xO mx) (shift_pos (Z.to_pos prec) Coq_xH) + if Pos.eqb (Coq_xO mx) + (Pos.iter (fun x0 -> Coq_xO x0) Coq_xH (Z.to_pos prec)) then coq_SFldexp prec emax (coq_SFone prec emax) (fexp prec emax (Z.sub (snd (coq_SFfrexp prec emax x)) (Zpos Coq_xH))) @@ -526,7 +534,8 @@ let coq_SFpred_pos prec emax x = match x with (** val coq_SFmax_float : coq_Z -> coq_Z -> spec_float **) let coq_SFmax_float prec emax = - S754_finite (false, (Pos.sub (shift_pos (Z.to_pos prec) Coq_xH) Coq_xH), + S754_finite (false, + (Pos.sub (Pos.iter (fun x -> Coq_xO x) Coq_xH (Z.to_pos prec)) Coq_xH), (Z.sub emax prec)) (** val coq_SFsucc : coq_Z -> coq_Z -> spec_float -> spec_float **) diff --git a/template-coq/specFloat.patch b/template-coq/specFloat.patch index 294627074..f485afd40 100644 --- a/template-coq/specFloat.patch +++ b/template-coq/specFloat.patch @@ -2,8 +2,8 @@ +++ gen-src/specFloat.ml 2020-12-04 21:48:33.000000000 +0100 @@ -4,6 +4,7 @@ open Datatypes - open Zbool - open Zpower + open IntDef + open PosDef +open Float64 type spec_float = diff --git a/template-coq/src/ast_denoter.ml b/template-coq/src/ast_denoter.ml index 4accda36a..f31e38694 100644 --- a/template-coq/src/ast_denoter.ml +++ b/template-coq/src/ast_denoter.ml @@ -232,7 +232,7 @@ struct let unquote_universe_level evm l = evm, unquote_level l let unquote_universe_instance(evm: Evd.evar_map) (l: quoted_univ_instance): Evd.evar_map * UVars.Instance.t - = (evm, UVars.Instance.of_array ([||], Array.of_list (List0.map unquote_level l))) + = (evm, UVars.Instance.of_array ([||], Array.of_list (List.map unquote_level l))) let unquote_global_reference (trm : Kernames.global_reference) : GlobRef.t = diff --git a/template-coq/theories/Constants.v b/template-coq/theories/Constants.v index a8ea5dd3e..ede296051 100644 --- a/template-coq/theories/Constants.v +++ b/template-coq/theories/Constants.v @@ -43,15 +43,15 @@ Register Stdlib.Init.Specif.sigT as metacoq.sigma.type. Register Stdlib.Init.Specif.existT as metacoq.sigma.intro. Register MetaCoq.Template.TemplateMonad.Common.existT_typed_term as metacoq.sigma.typed_term. -Register Stdlib.Numbers.BinNums.positive as metacoq.pos.type. -Register Stdlib.Numbers.BinNums.xI as metacoq.pos.xI. -Register Stdlib.Numbers.BinNums.xO as metacoq.pos.xO. -Register Stdlib.Numbers.BinNums.xH as metacoq.pos.xH. - -Register Stdlib.Numbers.BinNums.Z as metacoq.Z.type. -Register Stdlib.Numbers.BinNums.Zpos as metacoq.Z.pos. -Register Stdlib.Numbers.BinNums.Zneg as metacoq.Z.neg. -Register Stdlib.Numbers.BinNums.Z0 as metacoq.Z.zero. +Register BinNums.positive as metacoq.pos.type. +Register BinNums.xI as metacoq.pos.xI. +Register BinNums.xO as metacoq.pos.xO. +Register BinNums.xH as metacoq.pos.xH. + +Register BinNums.Z as metacoq.Z.type. +Register BinNums.Zpos as metacoq.Z.pos. +Register BinNums.Zneg as metacoq.Z.neg. +Register BinNums.Z0 as metacoq.Z.zero. (* Ast *) Register MetaCoq.Common.BasicAst.relevance as metacoq.ast.relevance. diff --git a/test-suite/safechecker_test.v b/test-suite/safechecker_test.v index 542cec8e2..44cc847d0 100644 --- a/test-suite/safechecker_test.v +++ b/test-suite/safechecker_test.v @@ -12,7 +12,8 @@ Environment is well-formed and Ind(Stdlib.Init.Datatypes.nat,0,[]) has type: Sor MetaCoq SafeCheck (3 + 1). Definition bool_list := List.map negb (cons true (cons false nil)). -MetaCoq SafeCheck bool_list. +(* was working a bit by accident *) +(* MetaCoq SafeCheck bool_list. *) MetaCoq CoqCheck bool_list. (* Time MetaCoq SafeCheck @infer_and_print_template_program. *) diff --git a/utils/theories/bytestring.v b/utils/theories/bytestring.v index ad0f13089..a0b6ea0cf 100644 --- a/utils/theories/bytestring.v +++ b/utils/theories/bytestring.v @@ -9,7 +9,7 @@ Require Coq.Strings.String ssrbool. Require Import ssreflect. Require Import Coq.NArith.NArith. -Require Import Coq.micromega.Lia. +From Coq Require Import Lia. From Equations Require Import Equations. Set Primitive Projections. Set Default Proof Using "Type". @@ -196,7 +196,7 @@ Notation "x ++ y" := (String.append x y) : bs_scope. Import String. (** comparison *) -Require Import Orders Coq.Structures.OrderedType Coq.Structures.OrdersAlt. +From Coq Require Import Orders OrderedType OrdersAlt. Lemma to_N_inj : forall x y, Byte.to_N x = Byte.to_N y <-> x = y. Proof.