diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 3 |
1 files changed, 3 insertions, 0 deletions
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 |