From 899ea67188560571fe7c63645cac8523a23058ce Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 11 Jun 2021 21:55:44 -0400 Subject: [PATCH] post-rebase fix --- src/core/Sidekick_core.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 2d84a8a5..59efd05a 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -630,7 +630,7 @@ module type SOLVER_INTERNAL = sig and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number, returns [Some (const (x+y))], and [None] otherwise. *) - val normalize : t -> term -> term + val normalize : t -> term -> (term * P.t) option (** Normalize a term using all the hooks. This performs a fixpoint, i.e. it only stops when no hook applies anywhere inside the term. *)