diff options
Diffstat (limited to 'plugins/ssr/ssrcommon.mli')
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 9ba23467e7..566a933522 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -212,8 +212,7 @@ val pf_abs_prod : EConstr.t -> Goal.goal Evd.sigma * EConstr.types val mkSsrRRef : string -> Glob_term.glob_constr * 'a option -val mkSsrRef : string -> GlobRef.t -val mkSsrConst : +val mkSsrConst : string -> env -> evar_map -> evar_map * EConstr.t val pf_mkSsrConst : |