We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 9536705 commit ae418d4Copy full SHA for ae418d4
share/rocq-autosubst-ocaml/unscoped.v
@@ -1,12 +1,6 @@
1
(** * Autosubst Header for Unnamed Syntax
2
+*)
3
-Version: December 11, 2019.
4
- *)
5
-
6
-(* Adrian:
7
- I changed this library a bit to work better with my generated code.
8
- 1. I use nat directly instead of defining fin to be nat and using Some/None as S/O
9
- 2. I removed the "s, sigma" notation for scons because it interacts with dependent function types "forall x, A"*)
10
Require Import core.
11
Require Import Setoid Morphisms Relation_Definitions.
12
0 commit comments