Reactivating option "Set Printing Existential Instances" for asking printing full instances.

5 files changed, 14 insertions, 9 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index c12f8a276..49335a803 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -24,8 +24,8 @@ open Genarg
 open Clenv
 open Universes
 
-let _ = Constrextern.print_evar_arguments := true
-let _ = Constrextern.print_universes := true
+let _ = Detyping.print_evar_arguments := true
+let _ = Detyping.print_universes := true
 let _ = set_bool_option_value ["Printing";"Matching"] false
 let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fc4056962..39783a1e7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -39,8 +39,8 @@ open Decl_kinds
 (* This governs printing of local context of references *)
 let print_arguments = ref false
 
-(* If true, prints local context of evars, whatever print_arguments *)
-let print_evar_arguments = ref false
+(* If true, prints local context of evars *)
+let print_evar_arguments = Detyping.print_evar_arguments
 
 (* This governs printing of implicit arguments.  When
    [print_implicits] is on then [print_implicits_explicit_args] tells
@@ -141,8 +141,7 @@ let insert_pat_alias loc p = function
 (**********************************************************************)
 (* conversion of references                                           *)
 
-let extern_evar loc n l =
-(*  if !print_evar_arguments then*) CEvar (loc,n,l) (*else CEvar (loc,n,None)*)
+let extern_evar loc n l = CEvar (loc,n,l)
 
 (** We allow customization of the global_reference printer.
     For instance, in the debugger the tables of global references
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 89589bfac..7a1f155bd 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -31,6 +31,9 @@ let dl = Loc.ghost
 (** Should we keep details of universes during detyping ? *)
 let print_universes = Flags.univ_print
 
+(** If true, prints local context of evars, whatever print_arguments *)
+let print_evar_arguments = ref false
+
 let add_name na b t (nenv, env) = add_name na nenv, push_rel (na, b, t) env
 let add_name_opt na b t (nenv, env) = 
   match t with
@@ -508,7 +511,7 @@ let rec detype flags avoid env sigma t =
           let id = Evd.evar_ident evk sigma in
           let l = Evd.evar_instance_array bound_to_itself (Evd.find sigma evk) cl in
           let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> (Id.Set.union fvs (collect_vars c), Int.Set.union rels (free_rels c))) (Id.Set.empty,Int.Set.empty) l in
-          let l = Evd.evar_instance_array (fun id c -> bound_to_itself id c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs))) (Evd.find sigma evk) cl in
+          let l = Evd.evar_instance_array (fun id c -> not !print_evar_arguments && (bound_to_itself id c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
           id,l
         with Not_found ->
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)), 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 064b6a5ae..9657e5562 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -19,6 +19,9 @@ open Evd
 (** Should we keep details of universes during detyping ? *)
 val print_universes : bool ref
 
+(** If true, prints full local context of evars *)
+val print_evar_arguments : bool ref
+
 val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
 
 val subst_glob_constr : substitution -> glob_constr -> glob_constr
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 34538f21f..93c12c335 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