Skip to content

C
cfml
Commit 1d9dbd2e authored by Armaël Guéneau's avatar Armaël Guéneau
Browse files
Options

Coq 8.9 compat: Require Import ZArith.BinIntDef to get numeral notations for Z

parent bb9c876d
Hide whitespace changes
Inline Side-by-side
Showing with 1 addition and 1 deletion
generator/characteristic.ml
View file @ 1d9dbd2e
......@@ -1662,7 +1662,7 @@ let cfg_file str =
[ Cftop_coqs ([
Coqtop_set_implicit_args;
Coqtop_require [ "Coq.ZArith.BinInt"; "TLC.LibLogic"; "TLC.LibRelation"; "TLC.LibInt"; "TLC.LibListZ"; "CFML.Shared"; "CFML.CFHeaps"; "CFML.CFApp"; "CFML.CFPrint"; "CFML.CFBuiltin" ];
Coqtop_require_import [ "CFML.CFHeader" ];
Coqtop_require_import [ "Coq.ZArith.BinIntDef"; "CFML.CFHeader" ];
Coqtop_custom "Delimit Scope Z_scope with Z.";
Coqtop_custom "Local Open Scope cfheader_scope.";
(*DEPRECATED Coqtop_custom "Open Scope list_scope.";*)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment