diff options
| author | Maxime Dénès | 2017-04-11 00:28:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-11 00:28:47 +0200 |
| commit | 835be3a05e28eb6e26f703a034f22b2c6c61acaa (patch) | |
| tree | 00ecf04840ba027c3c71f8503d9811c8a5dc1d2e /plugins/ltac/tactic_debug.mli | |
| parent | 0980dbb1740c8d48d8ff0c516929f27f8cea854d (diff) | |
| parent | 2e6a89238dc7197057d0da80a16f4b4b1e41bfd8 (diff) | |
Merge PR#379: Introducing evar-insensitive constrs
Diffstat (limited to 'plugins/ltac/tactic_debug.mli')
| -rw-r--r-- | plugins/ltac/tactic_debug.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 520fb41eff..7745d9b7b6 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -11,6 +11,7 @@ open Pattern open Names open Tacexpr open Term +open EConstr open Evd (** TODO: Move those definitions somewhere sensible *) @@ -34,7 +35,7 @@ val debug_prompt : val db_initialize : unit Proofview.NonLogical.t (** Prints a constr *) -val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t +val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLogical.t (** Prints the pattern rule *) val db_pattern_rule : @@ -42,10 +43,10 @@ val db_pattern_rule : (** Prints a matched hypothesis *) val db_matched_hyp : - debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t + debug_info -> env -> evar_map -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t (** Prints the matched conclusion *) -val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t +val db_matched_concl : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLogical.t (** Prints a success message when the goal has been matched *) val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t |