Skip to content
Snippets Groups Projects

fix various uses of generated names

Closed Ralf Jung requested to merge ralf/mangle into master
12 files
+ 30
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