From c531096f97179db81f5b073b4eae2cec29e5fe25 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 24 Mar 2021 14:16:17 -0700 Subject: [PATCH] [sledge] Make name arg of Var.identified non-optional Reviewed By: jvillard Differential Revision: D27262515 fbshipit-source-id: fa9bafd30 --- sledge/src/fol/trm.ml | 2 +- sledge/src/fol/var_intf.ml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index 944fd0b31..8e654e84f 100644 --- a/sledge/src/fol/trm.ml +++ b/sledge/src/fol/trm.ml @@ -167,7 +167,7 @@ module Var = struct let freshen v ~wrt = fresh (name v) ~wrt - let identified ?(name = "") ~id = + let identified ~name ~id = assert (id > 0) ; make ~id:(id - Int.max_int) ~name diff --git a/sledge/src/fol/var_intf.ml b/sledge/src/fol/var_intf.ml index 17e7ba1fe..9f2144faa 100644 --- a/sledge/src/fol/var_intf.ml +++ b/sledge/src/fol/var_intf.ml @@ -33,9 +33,9 @@ module type S = sig val name : t -> string val fresh : string -> wrt:Set.t -> t * Set.t - val identified : ?name:string -> id:int -> t - (** Create a variable identified by [id] with optional [name]. The [id] - uniquely identifies the variable, and must be positive. *) + val identified : name:string -> id:int -> t + (** Create a variable identified by [id]. The [id] uniquely identifies the + variable, and must be positive. *) (** Variable renaming substitutions *) module Subst : Subst.S with type var := t with type set := Set.t