diff options
| -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 e4cca2679..8ca40f829 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 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 diff --git a/test-suite/bugs/closed/4464.v b/test-suite/bugs/closed/4464.v new file mode 100644 index 000000000..f8e9405d9 --- /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. |