From 1c8fd0f7134bcc295e31613c981ef4ef2c21af35 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 19 Oct 2018 13:16:25 +0200
Subject: Replace type sign = bool with SPlus | SMinus

---
 plugins/ltac/g_tactic.mlg | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 7bf705ffeb..574e22d50e 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -147,7 +147,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
     end
   | _ -> ElimOnConstr clbind
 
-let mkNumeral n = Numeral (string_of_int (abs n), 0<=n)
+let mkNumeral n =
+  Numeral ((if 0<=n then SPlus else SMinus),string_of_int (abs n))
 
 let mkTacCase with_evar = function
   | [(clear,ElimOnConstr cl),(None,None),None],None ->
-- 
cgit v1.2.3