Syntactic Definition autorisée dans les motifs de Cases (utile notamment

pour fusionner eq et eqT)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2628 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 25 insertions, 18 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 54816fb036..c8aa762449 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -180,24 +180,31 @@ type pattern_qualid_kind =
 let maybe_constructor env = function
   | Node(loc,"QUALID",l) ->
       let qid = interp_qualid l in
-      (try 
-	match kind_of_term (global_qualified_reference qid) with 
-	  | Construct c -> 
-	      if !dump then add_glob loc (ConstructRef c); 
-	      ConstrPat (loc,c)
-	  | _ -> 
-	      (match maybe_variable l with
-		 | Some s -> 
-		     warning ("Defined reference "^(string_of_qualid qid)
-			      ^" is here considered as a matching variable");
-		     VarPat (loc,s)
-		 | _ -> error ("This reference does not denote a constructor: "
-			       ^(string_of_qualid qid)))
-      with Not_found -> 
-	match maybe_variable l with
-	  | Some s -> VarPat (loc,s)
-	  | _ -> error ("Unknown qualified constructor: "
-			^(string_of_qualid qid)))
+      (try match extended_locate qid with
+       | SyntacticDef sp ->
+	   (match Syntax_def.search_syntactic_definition sp with
+	    | RRef (_,(ConstructRef c as x)) ->
+		if !dump then add_glob loc x; 
+ 		ConstrPat (loc,c)
+	    | _ -> 
+		user_err_loc (loc,"maybe_constructor",
+           str "This syntactic definition should be aliased to a constructor"))
+       | TrueGlobal (ConstructRef c as r) -> 
+	   if !dump then add_glob loc r; 
+	   ConstrPat (loc,c)
+       | _ -> 
+	   (match maybe_variable l with
+	    | Some s -> 
+		warning ("Defined reference "^(string_of_qualid qid)
+			 ^" is here considered as a matching variable");
+		VarPat (loc,s)
+	    | _ -> error ("This reference does not denote a constructor: "
+			  ^(string_of_qualid qid)))
+       with Not_found -> 
+	 match maybe_variable l with
+	   | Some s -> VarPat (loc,s)
+	   | _ -> error ("Unknown qualified constructor: "
+			 ^(string_of_qualid qid)))
 
   (* This may happen in quotations *)
   | Node(loc,"MUTCONSTRUCT",[sp;Num(_,ti);Num(_,n)]) ->