diff options
| author | herbelin | 2012-02-01 08:57:50 +0000 |
|---|---|---|
| committer | herbelin | 2012-02-01 08:57:50 +0000 |
| commit | 3be4b91c09e6ec816aada997fc245484abfa1f05 (patch) | |
| tree | 93bf666115190587026f183325b508f549d5d7ef /dev/base_include | |
| parent | f7dba1c53fec7fe7ecefc4758e5a39c0010118b6 (diff) | |
Debugger vs tracer: Two different behaviors wrt printing: The debugger
runs in separate process. It has no access to the global env and it
should not request it. The tracer runs in the same process as Coq and
has full access to the global env and to regular pretty-printing of
global names.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14958 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/dev/base_include b/dev/base_include index d112596502..1c794a3ae9 100644 --- a/dev/base_include +++ b/dev/base_include @@ -199,6 +199,11 @@ let current_goal () = get_nth_goal 1;; let pf_e gl s = Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);; +(* Set usual printing since the global env is available from the tracer *) +let _ = Constrextern.in_debugger := false +let _ = Constrextern.set_debug_global_reference_printer + (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; + open Toplevel let go = loop |