From 67e93e9ff5e5b1723ff62da8a82782e5030b5721 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 31 Mar 2019 15:00:00 -0400
Subject: [numeral] Add a case for IndRef in constr_of_glob

Fixes #9840
---
 interp/notation.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index cdc2594454..b5e91b17e6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -632,6 +632,9 @@ let rec constr_of_glob env sigma g = match DAst.get g with
   | Glob_term.GRef (ConstructRef c, _) ->
       let sigma,c = Evd.fresh_constructor_instance env sigma c in
       sigma,mkConstructU c
+  | Glob_term.GRef (IndRef c, _) ->
+      let sigma,c = Evd.fresh_inductive_instance env sigma c in
+      sigma,mkIndU c
   | Glob_term.GApp (gc, gcl) ->
       let sigma,c = constr_of_glob env sigma gc in
       let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
-- 
cgit v1.2.3