diff options
| -rw-r--r-- | dev/top_printers.ml | 1 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 13 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_10026.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_3754.v (renamed from test-suite/bugs/opened/bug_3754.v) | 4 |
5 files changed, 12 insertions, 12 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 816316487c..2cd8cc3a74 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -27,7 +27,6 @@ open Clenv let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false -let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found) (* std_ppcmds *) let pp x = Pp.pp_with !Topfmt.std_ft x diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 062e3ca8b2..82726eccf0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -708,9 +708,6 @@ type binder_kind = BProd | BLambda | BLetIn (**********************************************************************) (* Main detyping function *) -let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable.")) -let set_detype_anonymous f = detype_anonymous := f - let detype_level sigma l = let l = hack_qualid_of_univ_level sigma l in GType (UNamed l) @@ -732,11 +729,13 @@ and detype_r d flags avoid env sigma t = match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with - | Name id -> GVar id - | Anonymous -> GVar (!detype_anonymous n) + | Name id -> GVar id + | Anonymous -> + let s = "_ANONYMOUS_REL_"^(string_of_int n) in + GVar (Id.of_string s) with Not_found -> - let s = "_UNBOUND_REL_"^(string_of_int n) - in GVar (Id.of_string s)) + let s = "_UNBOUND_REL_"^(string_of_int n) + in GVar (Id.of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) if n = Constr_matching.special_meta then diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 1a8e97efb8..00b0578a52 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -68,9 +68,6 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> clo val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option -(* XXX: This is a hack and should go away *) -val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit - val force_wildcard : unit -> bool val synthetize_type : unit -> bool diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v new file mode 100644 index 0000000000..0d3142d0f2 --- /dev/null +++ b/test-suite/bugs/closed/bug_10026.v @@ -0,0 +1,3 @@ +Require Import Coq.Lists.List. +Set Debug RAKAM. +Check fun _ => fold_right (fun A B => prod A B) unit _. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/closed/bug_3754.v index 18820b1a4c..7031cbf132 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/closed/bug_3754.v @@ -281,5 +281,7 @@ Defined. (factor2 fact)). rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. - Fail rewrite (concat_Ap ff2). + rewrite (concat_Ap ff2). Abort. + +End Factorization. |