| Age | Commit message (Collapse) | Author |
|---|
|
Almost all of ml4 were removed in the process. The only remaining files
are in the test-suite and probably need a bit of fiddling with coq_makefile,
and there only two really remaning ml4 files containing code.
|
|
|
|
Those optional arguments did not really make sense. It was pretty clear from
our code base, as all instances where triplicating the same type for TYPED,
RAW_TYPED and GLOB_TYPED.
|
|
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
|
We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.
Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.
The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.
|
|
|
|
|
|
longer use camlp4.
|
|
To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.
This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.
|
|
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
|
|
|
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
|
|
|
|
In the previous setting, all plugins/ltac/*.cmxs except ltac_plugin.cmxs
(for instance coretactics.cmxs, g_auto.cmxs, ...) were utterly bogus :
- wrong -for-pack used for their inner .cmx
- dependency over modules not provided (for instance Tacenv, that ends
up being a submodule of the pack ltac_plugin).
But we were lucky, those files were actually never loaded, thanks to the
several DECLARE PLUGIN inside coretactics and co, that end up in ltac_plugin,
and hence tell Coq that these modules are already known, preventing
any attempt to load them.
Anyway, this commit cleans up this mess (thanks PMP for the help)
|
|
|
|
|
|
Reminder of (some of) the reasons for removal:
- Despite the claim in sigma.mli, it does *not* prevent evar
leaks, something like:
fun env evd ->
let (evd',ev) = new_evar env evd in
(evd,ev)
will typecheck even with Sigma-like type annotations (with a proof of
reflexivity)
- The API stayed embryonic. Even typing functions were not ported to
Sigma.
- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
at all (despite still being so).
- There was no good story for higher order functions manipulating evar
maps. Without higher order, one can most of the time get away with
reusing the same name for the updated evar map.
- Most of the code doing complex things with evar maps was using unsafe
casts to sigma. This code should be fixed, but this is an orthogonal
issue.
Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
|
|
|
|
|
|
|
|
We make apparent in the API that the implicit tactic is set or not. This was
costing a lot in Pretyping for no useful reason, as it is almost always unset
and the default implementation was just failing immediately.
|
|
|
|
Tactic Notation
|
|
This commit is essentially moving files around. In particular, the corresponding
plugin still relies on a mllib file rather than a mlpack one. Otherwise, this
causes link-time issues for third-party plugins depending on modules defined
in the Ltac plugin.
|
