aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/vernacentries.ml4
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