diff options
| author | Pierre-Marie Pédrot | 2018-10-31 11:56:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-31 11:56:33 +0100 |
| commit | e29dc5ab5e85eb5f740de83f9f0b97b233651a3e (patch) | |
| tree | f3ec09aac5f5d26d88a1ae1cc7f3dff8bed2b861 /plugins | |
| parent | 47306462b9ddba0bfe43a2777e45549e0f7e3923 (diff) | |
| parent | 3f740f401652423b0182b9177c450a63337c7631 (diff) | |
Merge PR #8688: Generalizing the various evar_map printers in Termops over an environment
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9f7669f1d5..8b2721ae4e 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1492,7 +1492,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul if not (Evd.is_defined acc ev) then user_err ~hdr:"rewrite" (str "Unsolved constraint remaining: " ++ spc () ++ - Termops.pr_evar_info (Evd.find acc ev)) + Termops.pr_evar_info env acc (Evd.find acc ev)) else Evd.remove acc ev) cstrs evars' in |