diff options
| author | Maxime Dénès | 2017-06-20 08:09:00 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-20 08:09:00 +0200 |
| commit | 25cd7acea0df79fcc07274e429c9839de1246611 (patch) | |
| tree | 1ee95df49ec9ea7152afed41df425ea4e4760736 /plugins/rtauto | |
| parent | c7ac5dc8036623a02ab4ad6d11469e040e78c004 (diff) | |
| parent | 0437339ccac602d692b5b8c071b77ac756805520 (diff) | |
Merge PR#803: Clean ssr
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/refl_tauto.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index ac260e51ac..801fc46067 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -14,13 +14,13 @@ type atom_env= mutable env:(Term.constr*int) list} val make_form : atom_env -> - Proof_type.goal Evd.sigma -> EConstr.types -> Proof_search.form + Goal.goal Evd.sigma -> EConstr.types -> Proof_search.form val make_hyps : atom_env -> - Proof_type.goal Evd.sigma -> + Goal.goal Evd.sigma -> EConstr.types list -> EConstr.named_context -> (Names.Id.t * Proof_search.form) list -val rtauto_tac : Proof_type.tactic +val rtauto_tac : Tacmach.tactic |