diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-07 18:06:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-07 18:08:10 +0200 |
| commit | d93e8a7e7c9ae08cfedaf4a3db00ae3f9240bfe5 (patch) | |
| tree | ac5cd2cfb5a545f9374eb3155dc3ff20a5119104 /tactics | |
| 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.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0629935e1..893f33f1a 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 |