Skip to content
Snippets Groups Projects
Commit abbd8d0e authored by Ralf Jung's avatar Ralf Jung
Browse files

test with name mangling on CI

parent 03304222
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
.gitlab-ci.yml
+ 1
− 0
View file @ abbd8d0e
...@@ -31,6 +31,7 @@ build-coq.dev: ...@@ -31,6 +31,7 @@ build-coq.dev:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version dev" OPAM_PINS: "coq version dev"
MANGLE_NAMES: "1"
CI_COQCHK: "1" CI_COQCHK: "1"
build-coq.8.12.0: build-coq.8.12.0:
......
tests/telescopes.v
+ 2
− 0
View file @ abbd8d0e
From stdpp Require Import tactics telescopes. From stdpp Require Import tactics telescopes.
Local Unset Mangle Names. (* for stable goal printing *)
Section accessor. Section accessor.
(* This is like Iris' accessors, but in Prop. Just to play with telescopes. *) (* This is like Iris' accessors, but in Prop. Just to play with telescopes. *)
Definition accessor {X : tele} (α β γ : X → Prop) : Prop := Definition accessor {X : tele} (α β γ : X → Prop) : Prop :=
......
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