From 99129d2518bd9fe92051aa89138cbb57c839a270 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 28 Feb 2018 09:43:06 +0100 Subject: [ssreflect] Fix module scoping problems due to packing and mli files. Unfortunately, mli-only files cannot be included in packs, so we have the weird situation that the scope for `Tacexpr` is wrong. So we cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the global namespace instead. This creates problem when using other modular build/packing strategies [such as #6857] This could be indeed considered a bug in the OCaml compiler. In order to remedy this situation we face two choices: - leave the module out of the pack (!) - create an implementation for the module I chose the second solution as it seems to me like the most sensible choice. cc: #6512. --- plugins/funind/indfun.ml | 2 +- plugins/funind/indfun.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind') 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 -- cgit v1.2.3