diff options
| -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 |