diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/tacentries.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 188d5de7de..ac2d88dec2 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -697,7 +697,7 @@ type ('b, 'c) argument_interp = | ArgInterpFun : ('b, Val.t) interp_fun -> ('b, 'c) argument_interp | ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp | ArgInterpLegacy : - (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp + (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { arg_parsing : 'a Vernacextend.argument_rule; diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 79f9e093fb..309db539d0 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -125,7 +125,7 @@ type ('b, 'c) argument_interp = | ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c) argument_interp | ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp | ArgInterpLegacy : - (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp + (Geninterp.interp_sign -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { arg_parsing : 'a Vernacextend.argument_rule; |