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 /interp | |
| parent | 84694dcd9b720d4ed7eb838ad7c5a083e7eb86fe (diff) | |
Reactivating option "Set Printing Existential Instances" for asking printing full instances.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index fc40569624..39783a1e72 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 |