diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index b5228094..c3877c56 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -166,6 +166,18 @@ let _ = declare_bool_option optread = print_primproj_params; optwrite = (:=) print_primproj_params_value } +let print_primproj_compatibility_value = ref true +let print_primproj_compatibility () = !print_primproj_compatibility_value + +let _ = declare_bool_option + { optsync = true; + optdepr = false; + optname = "backwards-compatible printing of primitive projections"; + optkey = ["Printing";"Primitive";"Projection";"Compatibility"]; + optread = print_primproj_compatibility; + optwrite = (:=) print_primproj_compatibility_value } + + (* Auxiliary function for MutCase printing *) (* [computable] tries to tell if the predicate typing the result is inferable*) @@ -476,7 +488,7 @@ let rec detype flags avoid env sigma t = GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), [detype flags avoid env sigma c]) else - if Projection.unfolded p then + if print_primproj_compatibility () && Projection.unfolded p then (** Print the compatibility match version *) let c' = try |