diff options
Diffstat (limited to 'plugins/ssr/ssrast.mli')
| -rw-r--r-- | plugins/ssr/ssrast.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 0f4b86d10..94eaa1d6a 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -145,6 +145,6 @@ type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option) (* OOP : these are general shortcuts *) type gist = Tacintern.glob_sign type ist = Tacinterp.interp_sign -type goal = Proof_type.goal +type goal = Goal.goal type 'a sigma = 'a Evd.sigma -type v82tac = Proof_type.tactic +type v82tac = Tacmach.tactic |