diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-19 16:36:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-19 18:15:27 +0200 |
| commit | 666568377cbe1c18ce479d32f6359aa61af6d553 (patch) | |
| tree | 188217d9c0141ac95bab7bec24e021d13afc0084 /plugins/funind | |
| parent | c8986ad5589ad5bbed0936f9c16bba3f2ae1d2c4 (diff) | |
Type delayed_open_constr is now monotonic.
Diffstat (limited to 'plugins/funind')
| -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 eadeebd38..ab3629f89 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 |