Skip to content
Snippets Groups Projects

make sure std++ does not rely on generated names

Merged Ralf Jung requested to merge ci/ralf/mangle into master
1 unresolved thread
12 files
+ 31
26
Compare changes
  • Side-by-side
  • Inline
Files
12
+ 2
0
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 :=
Loading