Second step of integration of Program:

- Remove useless functorization of Pretyping
- Move Program coercion/cases code inside pretyping/, enabled according
to a flag.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 0 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 470cf81f18..29e01bac39 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -66,6 +66,9 @@ let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
 let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
 
+let program_mode = ref false
+let is_program_mode () = !program_mode
+
 let hash_cons_proofs = ref true
 
 let warn = ref true