From 4dc76691537c57cb8344e82d6bb493360ae12aaa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Sep 2007 09:42:04 +0000
Subject: - Fixing bug 1703 ("intros until n" falls back on the variable name
 when   the latter is bound to a var which is not a quantified one - this led 
  to remove a line marked "temporary compatibility" ... ; made a distinction  
 between quantified hypothesis as for "intros until" and binding names as   in
 "apply with"; in both cases, we now expect that a identifier not used   as a
 variable, as in "apply f_equal with f:=g" where "f" is a true binder   name
 in f_equal, must not be used as a variable elsewhere [see   corresponding
 change in Ints/Tactic.v]) - Fixing bug 1643 (bug in the algorithm used to
 possibly reuse a   global name in the recursive calls of a coinductive term)
 - Fixing bug 1699 (bug in contracting nested patterns at printing time   when
 the return clause of the subpatterns is dependent) - Fixing bug 1697 (bug in
 the TacAssert clause of Tacinterp.subst_tactic) - Fixing bug 1678 (bug in
 converting constr_pattern to constr in Constrextern)

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

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 763261bfd5..32d9f107cf 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -942,6 +942,8 @@ let rec raw_of_pat env = function
   | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
       let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
       RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
+  | PCase (_,PMeta None,tm,[||]) ->
+      RCases (loc,None,[raw_of_pat env tm,(Anonymous,None)],[])
   | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
       let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
       let brns = Array.to_list cstr_nargs in
-- 
cgit v1.2.3