diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index b65d9867d..9c350483b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -93,7 +93,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,Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None)) (args@c_list) encoded_pat_as_patlist in let princ' = Some (princ,bindings) in diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 93e03852e..dcc1c2ea6 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -14,7 +14,7 @@ val functional_induction : bool -> EConstr.constr -> (EConstr.constr * EConstr.constr bindings) option -> - Tacexpr.or_and_intro_pattern option -> + Ltac_plugin.Tacexpr.or_and_intro_pattern option -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma |