summaryrefslogtreecommitdiff
path: root/plugins/funind/functional_principles_types.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/functional_principles_types.mli')
-rw-r--r--plugins/funind/functional_principles_types.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index fb04c6ec..1c02c16e 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -27,8 +27,8 @@ val compute_new_princ_type_from_rel : constr array -> sorts array ->
exception No_graph_found
-val make_scheme : (constant*Rawterm.rawsort) list -> Entries.definition_entry list
+val make_scheme : (constant*Glob_term.glob_sort) list -> Entries.definition_entry list
-val build_scheme : (identifier*Libnames.reference*Rawterm.rawsort) list -> unit
-val build_case_scheme : (identifier*Libnames.reference*Rawterm.rawsort) -> unit
+val build_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) list -> unit
+val build_case_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) -> unit