diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-22 17:15:31 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-22 17:15:31 +0000 |
| commit | 03ae5e5a2feccb80e5510f9b0cd02db06bef484f (patch) | |
| tree | 3daf87720be67b3715fd795d1b1c1f453f00cbac /tactics/extraargs.ml4 | |
| parent | d33f10ce6dfc689da768f23360d46b88a57fc42e (diff) | |
Now, idtac closures use maps instead of association list.
The semantics changed slightly so it may break some scripts, though
it is very unlikely, as they would have to be quite intricated and
poorly written. Indeed, the test-suite passed just fine.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16604 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/extraargs.ml4')
| -rw-r--r-- | tactics/extraargs.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index da2660ae5..5dcbd73a8 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -63,7 +63,7 @@ let interp_occs ist gl l = match l with | ArgArg x -> x | ArgVar (_,id as locid) -> - (try int_list_of_VList (List.assoc id ist.lfun) + (try int_list_of_VList (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) let interp_occs ist gl l = Tacmach.project gl , interp_occs ist gl l |