diff options
| author | Emilio Jesus Gallego Arias | 2020-03-14 03:19:15 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:37 -0400 |
| commit | d507679b5b6dfac944e038b6a3ebd9fb8e6998ff (patch) | |
| tree | 4ddc9397465b1d563568f88d86c19f4e442f05c7 /vernac/declareDef.mli | |
| parent | 56ffe818ab7706a82d79b538fdf3af8b23d95f40 (diff) | |
[declareDef] Cleanup of allow_evars and check_evars
We don't the parameter anymore as the paths are too different now.
Note that this removes a duplicate `check_evars` that has been in
`master` quite some time [double check in `ComDefinition` and in
`DeclareDef.prepare_definition`]
Diffstat (limited to 'vernac/declareDef.mli')
| -rw-r--r-- | vernac/declareDef.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 27d9460382..f72954d8c2 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -110,8 +110,7 @@ val prepare_obligation -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info val prepare_parameter - : allow_evars:bool - -> poly:bool + : poly:bool -> udecl:UState.universe_decl -> types:EConstr.types -> Evd.evar_map |