diff options
| author | ppedrot | 2013-06-22 17:15:31 +0000 |
|---|---|---|
| committer | ppedrot | 2013-06-22 17:15:31 +0000 |
| commit | 03ae5e5a2feccb80e5510f9b0cd02db06bef484f (patch) | |
| tree | 3daf87720be67b3715fd795d1b1c1f453f00cbac /tactics/geninterp.ml | |
| 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/geninterp.ml')
| -rw-r--r-- | tactics/geninterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml index deba015362..cdb7dcb11b 100644 --- a/tactics/geninterp.ml +++ b/tactics/geninterp.ml @@ -14,7 +14,7 @@ open Genarg module TacStore = Store.Make(struct end) type interp_sign = { - lfun : (Id.t * tlevel generic_argument) list; + lfun : tlevel generic_argument Id.Map.t; extra : TacStore.t } type ('glb, 'top) interp_fun = interp_sign -> |