diff options
| author | Maxime Dénès | 2017-10-03 11:45:31 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-03 11:45:31 +0200 |
| commit | afe519db64b4864b5a901ab96a1e4297e9316b14 (patch) | |
| tree | 9fe22a04fcfd049081dedb6f9262a3a321176d03 /plugins/ltac/tacinterp.mli | |
| parent | e33cd69ab6fcb38478a6c0e00628a5de16181906 (diff) | |
| parent | b772c323f62b322c9b0a4ab90c7de8b1e2066bae (diff) | |
Merge PR #1040: Efficient fresh name generation
Diffstat (limited to 'plugins/ltac/tacinterp.mli')
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index c1ab2b4c49..d0a0a81d4c 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -40,7 +40,7 @@ type interp_sign = Geninterp.interp_sign = { lfun : value Id.Map.t; extra : TacStore.t } -val f_avoid_ids : Id.t list TacStore.field +val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field val extract_ltac_constr_values : interp_sign -> Environ.env -> @@ -113,7 +113,7 @@ val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic (** Globalization + interpretation *) -val interp_tac_gen : value Id.Map.t -> Id.t list -> +val interp_tac_gen : value Id.Map.t -> Id.Set.t -> debug_info -> raw_tactic_expr -> unit Proofview.tactic val interp : raw_tactic_expr -> unit Proofview.tactic |