diff options
| author | Pierre-Marie Pédrot | 2016-10-07 18:06:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-07 18:08:10 +0200 |
| commit | d93e8a7e7c9ae08cfedaf4a3db00ae3f9240bfe5 (patch) | |
| tree | ac5cd2cfb5a545f9374eb3155dc3ff20a5119104 | |
| parent | a2615bc47ed022ed4466741af3d4a29d45d05950 (diff) | |
Fix bug #4464: "Anomaly: variable H' unbound. Please report.".
We simply catch the RetypeError raised by the retyping function and translate
it into a user error, so that it is captured by the tactic monad instead of
reaching toplevel.
| -rw-r--r-- | pretyping/retyping.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4464.v | 4 |
3 files changed, 11 insertions, 1 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index e4cca2679c..8ca40f829f 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -46,3 +46,5 @@ val type_of_global_reference_knowing_conclusion : val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr + +val print_retype_error : retype_error -> Pp.std_ppcmds diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0629935e10..893f33f1a8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -48,7 +48,11 @@ let inj_with_occurrences e = (AllOccurrences,e) let dloc = Loc.ghost -let typ_of env sigma c = Retyping.get_type_of env (Sigma.to_evar_map sigma) c +let typ_of env sigma c = + let open Retyping in + try get_type_of ~lax:true env (Sigma.to_evar_map sigma) c + with RetypeError e -> + user_err_loc (Loc.ghost, "", print_retype_error e) open Goptions diff --git a/test-suite/bugs/closed/4464.v b/test-suite/bugs/closed/4464.v new file mode 100644 index 0000000000..f8e9405d93 --- /dev/null +++ b/test-suite/bugs/closed/4464.v @@ -0,0 +1,4 @@ +Goal True -> True. +Proof. + intro H'. + let H := H' in destruct H; try destruct H. |