From 666568377cbe1c18ce479d32f6359aa61af6d553 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 19 Oct 2015 16:36:53 +0200
Subject: Type delayed_open_constr is now monotonic.

---
 plugins/funind/indfun.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index eadeebd38e..ab3629f89e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -10,6 +10,7 @@ open Glob_term
 open Declarations
 open Misctypes
 open Decl_kinds
+open Sigma.Notations
 
 let is_rec_info scheme_info =
   let test_branche min acc (_,_,br) =
@@ -86,7 +87,7 @@ let functional_induction with_clean c princl pat =
       in
       let encoded_pat_as_patlist =
         List.make (List.length args + List.length c_list - 1) None @ [pat] in
-      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> sigma,(c,NoBindings))),(None,pat),None))
+      List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
         (args@c_list) encoded_pat_as_patlist
     in
     let princ' = Some (princ,bindings) in
-- 
cgit v1.2.3