diff options
| author | Pierre-Marie Pédrot | 2016-11-06 21:59:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:26:38 +0100 |
| commit | b77579ac873975a15978c5a4ecf312d577746d26 (patch) | |
| tree | 772e41667e74c38582ff6f4645c73e7d7556f935 /toplevel | |
| parent | 258c8502eafd3e078a5c7478a452432b5c046f71 (diff) | |
Tacred API using EConstr.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b480fcd868..1d82d9ae1c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1270,6 +1270,7 @@ let explain_pattern_matching_error env sigma = function let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) -> + let c = EConstr.to_constr sigma c in str "The abstracted term" ++ spc () ++ quote (pr_goal_concl_style_env env sigma c) ++ spc () ++ str "is not well typed." ++ fnl () ++ |