diff options
| author | msozeau | 2007-02-16 00:44:53 +0000 |
|---|---|---|
| committer | msozeau | 2007-02-16 00:44:53 +0000 |
| commit | 1989c3b93c8002d1bd794c934680737ba0867717 (patch) | |
| tree | 89501d1d1376533cfb05e92038ff983eb474ca57 | |
| parent | 011ea7d69260471ff810e9e286dba027792a3e4c (diff) | |
Add functionality to permit printing terms with references to anonymous variables, useful for debugging
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9652 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/detyping.ml | 5 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 2 |
2 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 04665e2825..a0071d5b6d 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -358,12 +358,15 @@ let detype_sort = function (**********************************************************************) (* Main detyping function *) +let detype_anonymous = ref (fun loc n -> anomaly "detype: index to an anonymous variable") +let set_detype_anonymous f = detype_anonymous := f + let rec detype (isgoal:bool) avoid env t = match kind_of_term (collapse_appl t) with | Rel n -> (try match lookup_name_of_rel n env with | Name id -> RVar (dl, id) - | Anonymous -> anomaly "detype: index to an anonymous variable" + | Anonymous -> !detype_anonymous dl n with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) in RVar (dl, id_of_string s)) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 7f979d6e6d..0e9166ac4c 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -44,7 +44,7 @@ val detype_sort : sorts -> rawsort val lookup_name_as_renamed : env -> constr -> identifier -> int option val lookup_index_as_renamed : env -> constr -> int -> int option - +val set_detype_anonymous : (loc -> int -> rawconstr) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool val force_if : case_info -> bool |