diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml (renamed from plugins/funind/rawterm_to_relation.ml) | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.mli (renamed from plugins/funind/rawterm_to_relation.mli) | 0 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml (renamed from plugins/funind/rawtermops.ml) | 0 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.mli (renamed from plugins/funind/rawtermops.mli) | 0 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef_plugin.mllib | 4 |
7 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 0616007950..ce224d1aac 100644 --- a/plugins/funind/rawterm_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -6,7 +6,7 @@ open Glob_term open Libnames open Indfun_common open Util -open Rawtermops +open Glob_termops let observe strm = if do_observe () diff --git a/plugins/funind/rawterm_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 5c91292bad..5c91292bad 100644 --- a/plugins/funind/rawterm_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/glob_termops.ml index 0cf91f38c0..0cf91f38c0 100644 --- a/plugins/funind/rawtermops.ml +++ b/plugins/funind/glob_termops.ml diff --git a/plugins/funind/rawtermops.mli b/plugins/funind/glob_termops.mli index b6c407a240..b6c407a240 100644 --- a/plugins/funind/rawtermops.mli +++ b/plugins/funind/glob_termops.mli diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6e063d3c17..f23fcd6134 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -300,7 +300,7 @@ let generate_principle on_error let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in try (* We then register the Inductive graphs of the functions *) - Rawterm_to_relation.build_inductive names funs_args funs_types recdefs; + Glob_term_to_relation.build_inductive names funs_args funs_types recdefs; if do_built then begin diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index f757bafcbc..7c32c1d20c 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -21,7 +21,7 @@ open Termops open Declarations open Environ open Glob_term -open Rawtermops +open Glob_termops (** {1 Utilities} *) diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mllib index 31818c3992..ec1f5436ca 100644 --- a/plugins/funind/recdef_plugin.mllib +++ b/plugins/funind/recdef_plugin.mllib @@ -1,7 +1,7 @@ Indfun_common -Rawtermops +Glob_termops Recdef -Rawterm_to_relation +Glob_term_to_relation Functional_principles_proofs Functional_principles_types Invfun |