diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-22 15:05:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-22 15:05:59 +0000 |
| commit | c939260137bef6002aad416632641c04601dc2b8 (patch) | |
| tree | 0d5ff0a50600d8b4faf06bbb7bb1e35367af9e42 /interp | |
| parent | 55606828d6d6790631908b33dd9b13373a7ed096 (diff) | |
Allègement de l'affichage des références par le printer si possible
(on garde des noms de la forme IND(name,i) et CONSTR(name,i,j) que
lorsqu'on ne sait pas le bon nom, i.e. pour les IND mutuels autres que
le premier et pour tous les constructeurs).
Pour un affichage complètement explicite des noms avec ocamldebug,
charger maintenant set_raw_db en plus de db.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9515 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 15 | ||||
| -rw-r--r-- | interp/constrextern.mli | 3 |
2 files changed, 17 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d38662294..96548df71 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -109,6 +109,8 @@ let extern_evar loc n = *) CEvar (loc,n) +let rawdebug = ref false + let raw_string_of_ref = function | ConstRef kn -> "CONST("^(string_of_con kn)^")" @@ -120,11 +122,22 @@ let raw_string_of_ref = function | VarRef id -> "SECVAR("^(string_of_id id)^")" +let short_string_of_ref = function + | VarRef id -> string_of_id id + | ConstRef cst -> string_of_label (pi3 (repr_con cst)) + | IndRef (kn,0) -> string_of_label (pi3 (repr_kn kn)) + | IndRef (kn,i) -> + "IND("^string_of_label (pi3 (repr_kn kn))^(string_of_int i)^")" + | ConstructRef ((kn,i),j) -> + "CONSTRUCT("^ + string_of_label (pi3 (repr_kn kn))^","^(string_of_int i)^","^(string_of_int j)^")" + let extern_reference loc vars r = try Qualid (loc,shortest_qualid_of_global vars r) with Not_found -> (* happens in debugger *) - Ident (loc,id_of_string (raw_string_of_ref r)) + let f = if !rawdebug then raw_string_of_ref else short_string_of_ref in + Ident (loc,id_of_string (f r)) (************************************************************************) (* Equality up to location (useful for translator v8) *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 0ffb8c333..9a9c55ec1 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -52,6 +52,9 @@ val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref +(* Debug printing options *) +val rawdebug : bool ref + (* This governs printing of implicit arguments. If [with_implicits] is on and not [with_arguments] then implicit args are printed prefixed by "!"; if [with_implicits] and [with_arguments] are both on the |