From 34f63d7d890921cce37f4d48f48cdb020f2ac988 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 26 Nov 2017 19:00:46 +0100
Subject: [proof] Embed evar_map in RefinerError exception.

The exception needs to carry aroud a pair of `env, sigma` so printing
is correct. This gets rid of a few global calls, and it is IMO the
right thing to do.

While we are at it, we incorporate some fixes to a couple of
additional printing functions missing the `env, sigma` pair.
---
 plugins/ltac/rewrite.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'plugins/ltac/rewrite.ml')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c0060c5a7c..1f2e5f7ac1 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2021,14 +2021,16 @@ let add_morphism glob binders m s n =
 (** Taken from original setoid_replace, to emulate the old rewrite semantics where
     lemmas are first instantiated and then rewrite proceeds. *)
 
-let check_evar_map_of_evars_defs evd =
+let check_evar_map_of_evars_defs env evd =
  let metas = Evd.meta_list evd in
  let check_freemetas_is_empty rebus =
   Evd.Metaset.iter
    (fun m ->
-     if Evd.meta_defined evd m then () else
-      raise
-	(Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m])))
+     if Evd.meta_defined evd m then ()
+     else begin
+       raise
+         (Logic.RefinerError (env, evd, Logic.UnresolvedBindings [Evd.meta_name evd m]))
+     end)
  in
   List.iter
    (fun (_,binding) ->
@@ -2063,7 +2065,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env =
   let c1 = if l2r then nf c' else nf c1
   and c2 = if l2r then nf c2 else nf c'
   and car = nf car and rel = nf rel in
-  check_evar_map_of_evars_defs sigma;
+  check_evar_map_of_evars_defs env sigma;
   let prf = nf prf in
   let prfty = nf (Retyping.get_type_of env sigma prf) in
   let sort = sort_of_rel env sigma but in
-- 
cgit v1.2.3