From 41d6548d171317a54ee220afa67a5b0b13f7e00b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 6 Apr 2004 14:06:52 +0000
Subject: Bug sur commit 1.44 dans find_constructor (Not_Found pas rattrape)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5640 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c46cad89be..a3448d74fe 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -510,12 +510,17 @@ let maybe_constructor ref =
               str " is understood as a pattern variable");
         VarPat (find_pattern_variable ref)
 
+let mustbe_constructor loc ref = 
+  try find_constructor ref
+  with (Environ.NotEvaluableConst _ | Not_found) ->
+    raise (InternalisationError (loc,NotAConstructor ref))
+
 let rec intern_cases_pattern scopes aliases tmp_scope = function
   | CPatAlias (loc, p, id) ->
       let aliases' = merge_aliases aliases id in
       intern_cases_pattern scopes aliases' tmp_scope p
   | CPatCstr (loc, head, pl) ->
-      let c,pl0 = find_constructor head in
+      let c,pl0 = mustbe_constructor loc head in
       let argscs =
 	simple_adjust_scopes (find_arguments_scope (ConstructRef c), pl) in
       let (idsl,pl') =
-- 
cgit v1.2.3