From 0bfa187edddb0de9bb75c55e1b3d0f08830c7ac8 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Wed, 5 Jun 2013 13:26:51 +0000 Subject: Replacing lists by maps in matching interpretation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16561 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 8537208773..b5586bbd9d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1110,7 +1110,7 @@ let (forward_interp_tactic, extern_interp) = Hook.make () let conclPattern concl pat tac gl = let constr_bindings = match pat with - | None -> [] + | None -> Id.Map.empty | Some pat -> try matches pat concl with PatternMatchingFailure -> error "conclPattern" in -- cgit v1.2.3