diff options
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 698ee4703..23c863cab 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -640,8 +640,7 @@ let explain_refiner_cannot_generalize env sigma ty = pr_leconstr_env env sigma ty ++ str "." let explain_no_occurrence_found env sigma c id = - let c = EConstr.to_constr sigma c in - str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++ + str "Found no subterm matching " ++ pr_leconstr_env env sigma c ++ str " in " ++ (match id with | Some id -> Id.print id |