From e03d1840a8e6eec927e7fbe006d59ab21b8d818f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 22 Oct 2008 11:21:45 +0000
Subject: Affichage des notations récursives: - Prise en compte des notations
 applicatives - Remplacement du codage des arguments liste des notations
 récursives   sous forme de terme par une représentation directe (permet
 notamment   de résoudre un problème de stack overflow de la fonction
 d'affichage) + Correction bug affichage Lemma dans ppvernac.ml + Divers
 util.ml

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

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 8bacbcd8cf..7801f048fe 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -58,7 +58,7 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
   in
   let rec aux bdvars l c = match c with
     | CRef (Ident (_,id)) -> found id bdvars l
-    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id))) :: _) when not (Idset.mem id bdvars) ->
+    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [])) when not (Idset.mem id bdvars) ->
 	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
     | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
   in aux bound l c
-- 
cgit v1.2.3