aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrparser.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrparser.ml4')
-rw-r--r--plugins/ssr/ssrparser.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 060225dab..1e1a986da 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -342,7 +342,7 @@ let interp_index ist gl idx =
| None ->
begin match Tacinterp.Value.to_constr v with
| Some c ->
- let rc = Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) c in
+ 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