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 ++-
 plugins/ssr/ssrparser.mlg | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins')

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 ->
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 0ec5f1673a..9931305832 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -360,8 +360,8 @@ let interp_index ist gl idx =
         | Some c ->
           let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in
           begin match Notation.uninterp_prim_token rc with
-          | _, Constrexpr.Numeral (s,b) ->
-             let n = int_of_string s in if b then n else -n
+          | _, Constrexpr.Numeral (b,s) ->
+             let n = int_of_string s in (match b with SPlus -> n | SMinus -> -n)
           | _ -> raise Not_found
           end
         | None -> raise Not_found
-- 
cgit v1.2.3