Add syntax for conditionally irrelevant types.

CoqHott · Nov 16, 2023 · cc4f036 · cc4f036
1 parent 6fa27fd
commit cc4f036
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/theories/AutoSubst/Ast.sig b/theories/AutoSubst/Ast.sig
@@ -1,6 +1,10 @@
 sort : Type
 term(tRel) : Type
 
+set : sort
+formula : sort
+irr : term -> sort
+
 tSort : sort -> term
 
 tProd : term -> (bind term in term) -> term