From 9a0c61b81a2d9c0024b20a6c7ad8af01026739b0 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Dec 2012 10:56:41 +0000 Subject: Moved Intset and Intmap to Int namespace. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/auto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/auto.ml') diff --git a/tactics/auto.ml b/tactics/auto.ml index 49841ecfa..ecc0930c1 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -823,7 +823,7 @@ let prepare_hint env (sigma,c) = (* We skip the test whether args is the identity or not *) let t = Evarutil.nf_evar sigma (existential_type sigma ev) in let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in - if not (Intset.is_empty (free_rels t)) then + if not (Int.Set.is_empty (free_rels t)) then error "Hints with holes dependent on a bound variable not supported."; if occur_existential t then (* Not clever enough to construct dependency graph of evars *) -- cgit v1.2.3