From da72fafac3b5b4b21330cd097f5728cbc127aea4 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 12 Sep 2020 09:15:06 +0200
Subject: Renaming Numeral into Number

---
 plugins/ssr/ssrparser.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 35fecfb0a5..ccdf5fa68e 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -350,7 +350,7 @@ 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 (None, []) with
-          | Constrexpr.Numeral n, _ when NumTok.Signed.is_int n ->
+          | Constrexpr.Number n, _ when NumTok.Signed.is_int n ->
             int_of_string (NumTok.Signed.to_string n)
           | _ -> raise Not_found
           end
-- 
cgit v1.2.3