From 6fe129a7617a8d80b14668389cd107af1c57a32a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr> Date: Mon, 26 Dec 2022 22:53:23 +0100 Subject: [PATCH] Rename [STRUCTURE_OPT] to [GSTRUCTURE_OPT]. --- src/Generalization.ml | 2 +- src/Generalization.mli | 2 +- src/Signatures.ml | 4 ++-- src/Structure.mli | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Generalization.ml b/src/Generalization.ml index f05e609..47418b5 100644 --- a/src/Generalization.ml +++ b/src/Generalization.ml @@ -11,7 +11,7 @@ open Signatures -module Make (S : STRUCTURE_OPT) = struct +module Make (S : GSTRUCTURE_OPT) = struct (* -------------------------------------------------------------------------- *) diff --git a/src/Generalization.mli b/src/Generalization.mli index 7f7a519..89d9454 100644 --- a/src/Generalization.mli +++ b/src/Generalization.mli @@ -22,7 +22,7 @@ open Signatures operations that allow constructing, inspecting, and instantiating schemes. *) module Make - (S : sig (** @inline *) include STRUCTURE_OPT end) + (S : sig (** @inline *) include GSTRUCTURE_OPT end) : sig (** {2 Unification} *) diff --git a/src/Signatures.ml b/src/Signatures.ml index 2cf4420..461a73e 100644 --- a/src/Signatures.ml +++ b/src/Signatures.ml @@ -190,10 +190,10 @@ module type GSTRUCTURE = sig end -(* [STRUCTURE_OPT] describes the output of [Structure.Option] and +(* [GSTRUCTURE_OPT] describes the output of [Structure.Option] and an input of [Generalization.Make]. *) -module type STRUCTURE_OPT = sig +module type GSTRUCTURE_OPT = sig module S : GSTRUCTURE diff --git a/src/Structure.mli b/src/Structure.mli index a3e02fb..1c52bd5 100644 --- a/src/Structure.mli +++ b/src/Structure.mli @@ -21,6 +21,6 @@ open Signatures module Option (S : sig (** @inline *) include GSTRUCTURE end) : sig (** @inline *) - include STRUCTURE_OPT with module S = S + include GSTRUCTURE_OPT with module S = S end -- GitLab