From 2d568a895d5c8a246f497c94c79811d3aad4269f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Jan 2016 00:20:46 +0100
Subject: Fixing #4467 (continued).

Function is_constructor was not properly fixed. Additionally, this fixes
a problem with the 8.5 interpretation of in-pattern (see Cases.v).
---
 interp/interp.mllib | 2 +-
 interp/topconstr.ml | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/interp.mllib b/interp/interp.mllib
index c9a0315267..96b52959a0 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -3,12 +3,12 @@ Constrarg
 Genintern
 Constrexpr_ops
 Notation_ops
-Topconstr
 Ppextend
 Notation
 Dumpglob
 Syntax_def
 Smartlocate
+Topconstr
 Reserve
 Impargs
 Implicit_quantifiers
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 560cd0277b..2cb2449b7d 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -39,7 +39,9 @@ let error_invalid_pattern_notation loc =
 (* Functions on constr_expr *)
 
 let is_constructor id =
-  try ignore (Nametab.locate_extended (qualid_of_ident id)); true
+  try Globnames.isConstructRef
+        (Smartlocate.global_of_extended_global
+           (Nametab.locate_extended (qualid_of_ident id)))
   with Not_found -> false
 
 let rec cases_pattern_fold_names f a = function
-- 
cgit v1.2.3