diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-22 15:21:01 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-22 15:21:01 +0000 |
| commit | 34e80b356fcccd938f114925e91c53cb33b2bd19 (patch) | |
| tree | 517da7072e340d0c36d05a2908079393e431dc43 /tactics/tacinterp.mli | |
| parent | bd7da353ea503423206e329af7a56174cb39f435 (diff) | |
Generalizing the use of maps instead of lists in the interpretation
of tactics.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16602 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 6affc21a4..32880fd77 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -45,8 +45,7 @@ val f_avoid_ids : Id.t list TacStore.field val f_debug : debug_info TacStore.field val extract_ltac_constr_values : interp_sign -> Environ.env -> - Pattern.constr_under_binders Id.Map.t * (Id.Map.key * Id.t option) list -(* should be Pretyping.ltac_var_map *) + Pretyping.ltac_var_map (** Tactic extensions *) val add_tactic : |