diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d7548fb1e70134a6b6a058a1f66cca3c0372a42c..8e9cb4d600d8a7c7060c89c4377112e5604d8f9e 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -31,6 +31,7 @@ build-coq.dev: <<: *template variables: OPAM_PINS: "coq version dev" + MANGLE_NAMES: "1" CI_COQCHK: "1" build-coq.8.12.0: diff --git a/tests/telescopes.v b/tests/telescopes.v index 207457b880937b2a7c500e4ff3786c660e1e4119..ede324c066e674a4f04c01e4e686deb49f73d954 100644 --- a/tests/telescopes.v +++ b/tests/telescopes.v @@ -1,5 +1,7 @@ From stdpp Require Import tactics telescopes. +Local Unset Mangle Names. (* for stable goal printing *) + Section accessor. (* This is like Iris' accessors, but in Prop. Just to play with telescopes. *) Definition accessor {X : tele} (α β γ : X → Prop) : Prop :=