diff options
| author | Hugo Herbelin | 2014-12-04 10:47:31 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-04 11:42:59 +0100 |
| commit | 9fc63bfa8c8e8bc3bf835ebb2d3d444c5a6d4f9f (patch) | |
| tree | ce0547f9ec401d865d9f012d684967b29f80c070 /toplevel | |
| parent | 84694dcd9b720d4ed7eb838ad7c5a083e7eb86fe (diff) | |
Reactivating option "Set Printing Existential Instances" for asking printing full instances.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 34538f21fd..93c12c3351 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1235,8 +1235,8 @@ let _ = optdepr = false; optname = "printing of existential variable instances"; optkey = ["Printing";"Existential";"Instances"]; - optread = (fun () -> !Constrextern.print_evar_arguments); - optwrite = (:=) Constrextern.print_evar_arguments } + optread = (fun () -> !Detyping.print_evar_arguments); + optwrite = (:=) Detyping.print_evar_arguments } let _ = declare_bool_option |