From b2a1329391bd7847085178d2738e62af215e45b5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 28 Mar 2019 20:54:17 +0100
Subject: [program] Allow evars in type of fixpoints.

This is the right thing to do until we refine the program architecture
a bit to use EConstr.

Closes #9163 .
---
 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 ad7c65b70c..350b2d2945 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -232,7 +232,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let hook = Lemmas.mk_hook (hook sigma) in
   (* XXX: Grounding non-ground terms here... bad bad *)
   let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
-  let fullctyp = EConstr.to_constr sigma typ in
+  let fullctyp = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   Obligations.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
     Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp
-- 
cgit v1.2.3