diff options
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 3899bc709..996e2b6af 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,7 +1,8 @@ open Printer open CErrors -open Util open Term +open Sorts +open Util open Constr open Vars open Namegen |