diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 3dbd43806..bf9da870e 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) = @@ -85,7 +86,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 |