From 6608f64f001f8f1a50b2dc41fefdf63c0b84b270 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 2 Nov 2018 00:17:47 +0100
Subject: Passing evar_map to evars_of_term rather than expecting the term to
 be evar-nf.

---
 vernac/comProgramFixpoint.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comProgramFixpoint.ml')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3befdc5885..69e2a209eb 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -243,7 +243,7 @@ let out_def = function
   | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.")
 
 let collect_evars_of_term evd c ty =
-  let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in
+  let evars = Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) in
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-- 
cgit v1.2.3