From 9903f6a7f86661549def884a0050d0f4537d52d7 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 28 Nov 2018 10:35:27 -0800
Subject: Add undocumented options from mattam82

---
 doc/sphinx/addendum/program.rst | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'doc/sphinx/addendum/program.rst')

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 429dcbee69..56f84d0ff0 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -95,6 +95,14 @@ coercions.
    (the option is on by default). Coercion of subset types and pairs is still
    active in this case.
 
+.. flag:: Program Mode
+
+   Enables the program mode, in which 1) typechecking allows subset coercions and
+   2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and
+   :cmd:`Program Definition` act
+   like Program Fixpoint/Definition, generating obligations if there are
+   unresolved holes after typechecking.
+
 .. _syntactic_control:
 
 Syntactic control over equalities
-- 
cgit v1.2.3