diff options
Diffstat (limited to 'plugins/rtauto/refl_tauto.mli')
| -rw-r--r-- | plugins/rtauto/refl_tauto.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index e5fb646a4..f7e6ec020 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -18,7 +18,7 @@ val make_hyps : atom_env -> Proof_type.goal Tacmach.sigma -> Term.types list -> - (Names.identifier * Term.types option * Term.types) list -> - (Names.identifier * Proof_search.form) list + (Names.Id.t * Term.types option * Term.types) list -> + (Names.Id.t * Proof_search.form) list val rtauto_tac : Proof_type.tactic |