Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt to https://github.com/coq/coq/pull/19530 #44

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Adapt to https://github.com/coq/coq/pull/19530 #44

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/reify.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ let get_fun_5 d s = let v = get_const d s in fun x y z t u -> force_app v [|x;y;
(* Coq constants *)
module Coq = struct
(* binary positive numbers *)
let positive_path = ["Coq" ; "Numbers"; "BinNums"]
let positive_path = ["Stdlib" ; "BinNums"; "BinNums"]
let positive = get_const positive_path "positive"
let xH = get_const positive_path "xH"
let xI = get_fun_1 positive_path "xI"
Expand Down
4 changes: 2 additions & 2 deletions theories/Common.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,11 @@
(** This small module is imported in all our files, it exports useful
modules and defines some basic utilities and tactics *)

From Coq Require Export Arith.

Check warning on line 12 in theories/Common.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev) 

"From Coq" has been replaced by "From Stdlib".
From Coq Require Export Lia.

Check warning on line 13 in theories/Common.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev) 

"From Coq" has been replaced by "From Stdlib".
From Coq Require Export BinNums BinPos PArith.Pnat.

Check warning on line 14 in theories/Common.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev) 

"From Coq" has been replaced by "From Stdlib".
From Coq Require Export Program.Equality.
From Coq Require Export Setoid Morphisms.
From Coq.Program Require Export Equality.

Check warning on line 15 in theories/Common.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev) 

Coq.Program has been replaced by Stdlib.Program.
From Coq Require Export Setoid Morphisms.

Check warning on line 16 in theories/Common.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:dev) 

"From Coq" has been replaced by "From Stdlib".

Set Implicit Arguments.

Expand Down
Loading