From 410b3cc1cc0f677e052cfedcee03e14521264b64 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 17 May 2016 17:24:57 +0200
Subject: Program: cleanup in cases, add options

Unset Program Generalized Coercion to avoid coercion of general
applications.
Unset Program Cases to deactivate generation equalities and
disequalities of cases.
---
 pretyping/program.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping/program.mli')

diff --git a/pretyping/program.mli b/pretyping/program.mli
index 765f355808..023ff8ca58 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -39,3 +39,5 @@ val mk_coq_not : constr -> constr
 val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr
 
 val get_proofs_transparency : unit -> bool
+val is_program_cases : unit -> bool
+val is_program_generalized_coercion : unit -> bool
-- 
cgit v1.2.3