From fc06cb87286e2b114c7f92500511d5914b8f7f48 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Jul 2010 21:06:18 +0000
Subject: Extension of the recursive notations mechanism - Added support for
 recursive notations with binders - Added support for arbitrary large
 iterators in recursive notations - More checks on the use of variables and
 improved error messages - Do side-effects in metasyntax only when sure that
 everything is ok - Documentation

Note: it seems there were a small bug in match_alist (instances obtained
from matching the first copy of iterator were not propagated).

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

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index cad48a5a1c..7dbffe6681 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -91,7 +91,7 @@ let is_freevar ids env x =
       with _ -> not (is_global x)
   with _ -> true
 
-(* Auxilliary functions for the inference of implicitly quantified variables. *)
+(* Auxiliary functions for the inference of implicitly quantified variables. *)
 
 let ungeneralizable loc id =
   user_err_loc (loc, "Generalization", 
@@ -108,7 +108,7 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
   in
   let rec aux bdvars l c = match c with
     | CRef (Ident (loc,id)) -> found loc 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