Add Ltac2.Constr.{is_float,is_uint63,is_array}
#17894
Merged
coqbot-app / GitLab CI job library:ci-geocoq (pull request)
completed
Jul 31, 2023 in 0s
Test has failed on GitLab CI
This job is allowed to fail.
This job ran on the Docker image registry.gitlab.com/coq/coq:bionic_coq-V2023-06-29-2b9dca3152, depended on the build job build:edge+flambda with OCaml 4.14.1+flambda.
We show below an excerpt from the trace from GitLab starting around the last detected "Error" (the complete trace is available here).
Details
File "./Meta_theory/Models/POF_to_Tarski.v", line 21, characters 0-64:
Error: Cannot find a physical path bound to logical path
GeoCoq.Meta_theory.Counter_models.nD.coplanarity.
Command exited with non-zero status 1
Meta_theory/Models/POF_to_Tarski.vo (real: 2.95, user: 1.17, sys: 0.33, mem: 602008 ko)
Makefile:823: recipe for target 'Meta_theory/Models/POF_to_Tarski.vo' failed
make[2]: *** [Meta_theory/Models/POF_to_Tarski.vo] Error 1
make[2]: *** Waiting for unfinished jobs....
File "./Meta_theory/Counter_models/Planar/gupta_inspired_to_independent_tarski.v", line 6, characters 0-68:
Warning: Notation "[ predI _ & _ ]" was already used in scope fun_scope.
[notation-overridden,parsing,default]
File "./Meta_theory/Counter_models/Planar/gupta_inspired_to_independent_tarski.v", line 6, characters 0-68:
Warning: Notation "[ predU _ & _ ]" was already used in scope fun_scope.
[notation-overridden,parsing,default]
File "./Meta_theory/Counter_models/Planar/gupta_inspired_to_independent_tarski.v", line 6, characters 0-68:
Warning: Notation "[ predD _ & _ ]" was already used in scope fun_scope.
[notation-overridden,parsing,default]
File "./Meta_theory/Counter_models/Planar/gupta_inspired_to_independent_tarski.v", line 6, characters 0-68:
Warning: Notation "[ predC _ ]" was already used in scope fun_scope.
[notation-overridden,parsing,default]
File "./Meta_theory/Counter_models/Planar/gupta_inspired_to_independent_tarski.v", line 6, characters 0-68:
Warning: Notation "[ preim _ of _ ]" was already used in scope fun_scope.
[notation-overridden,parsing,default]
File "./Meta_theory/Counter_models/Planar/gupta_inspired_to_independent_tarski.v", line 6, characters 0-68:
Warning: Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
File "./Meta_theory/Counter_models/Planar/gupta_inspired_to_independent_tarski.v", line 6, characters 0-68:
Warning: Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
File "./Meta_theory/Counter_models/Planar/gupta_inspired_to_independent_tarski.v", line 6, characters 0-68:
Warning: Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
File "./Meta_theory/Counter_models/Planar/gupta_inspired_to_independent_tarski.v", line 6, characters 0-68:
Warning: Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
File "./Meta_theory/Counter_models/Planar/gupta_inspired_to_independent_tarski.v", line 6, characters 0-68:
Warning: Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
File "./Meta_theory/Counter_models/Planar/gupta_inspired_to_independent_tarski.v", line 6, characters 0-68: