| Age | Commit message (Collapse) | Author |
|---|
|
I have removed the second field of the "Constrexpr.CRecord" variant
because once it was set to "None"
it never changed to anything else.
It was just carried and copied around.
|
|
|
|
The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.
Some missing comments were added to the *.mli file.
The output of ocamldoc was checked whether it looks in a reasonable way.
"TODO: cleanup" was removed
The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)
The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)
The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)
The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})
The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.
Thrown exceptions are now documented.
Naming of formal parameters was made more consistent across different functions.
Comments of similar functions in different modules are now consistent.
Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
we can see the comments also there and do not need to open a different file if we want to see it.)
When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)
"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)
An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
|
|
|
|
Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.
|
|
|
|
|
|
Actually the identifier was never used and just carried along.
|
|
The TacAlias node now only contains the arguments fed to the tactic notation.
The binding variables are worn by the tactic representation in Tacenv.
|
|
|
|
This commit has deep consequences in term of tactic evaluation,
as it allows to pass any tac_arg to ML and alias tactics rather than
mere generic arguments. This makes the evaluation much more uniform,
and in particular it removes the special evaluation function for notations.
This last point may break some notations out there unluckily.
I had to treat in an ad-hoc way the tactic(...) entry of tactic notations
because it is actually not interpreted as a generic argument but rather
as a proper tactic expression instead.
There is for now no syntax to pass any tactic argument to a given ML or
notation tactic, but this should come soon.
Also fixes bug #3849 en passant.
|
|
We also intepret it at toplevel as a true constr and push the resulting
evarmap in the current state.
|
|
The previous implementation was a source of evar leaks if misused, as
it created values coming together with their current evar_map. This is
dead wrong if the value is not used on the spot. To fix this, we rather
return a ['a delayed_open] object.
Two argument types were modified: bindings and constr_bindings. The
open_constr argument should also be fixed, but it is more entangled and
thus I leave it for another commit.
|
|
|
|
For instance, calling only Id.print is faster than calling both str and
Id.to_string, since the latter performs a copy. It also makes the code a
bit simpler to read.
|
|
Now that types can share the same dynamic representation, we do not have
to transtype the topelvel values dynamically and just take advantage of
the standard interpretation function.
|
|
|
|
|
|
|
|
|
|
The definition of Vernacexpr.VernacDeclareTacticDefinition was changed.
The original definition allowed us to represent non-sensical value such as:
VernacDeclareTacticDefinition(Qualid ..., false, ...)
The new definition prevents that.
|
|
command is mapped.
|
|
Originally, "VernacTime" and "VernacRedirect" were defined like this:
type vernac_expr =
...
| VernacTime of vernac_list
| VernacRedirect of string * vernac_list
...
where
type vernac_list = located_vernac_expr list
Currently, that list always contained one and only one element.
So I propose changing the definition of these two variants in the following way:
| VernacTime of located_vernac_expr
| VernacRedirect of string * located_vernac_expr
which covers all our current needs and enforces the invariant
related to the number of commands that are part of the
"VernacTime" and "VernacRedirect" variants.
|
|
|
|
|
|
|
|
It will later be used to fix a bug and improve some code.
Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
|
|
|
|
|
|
For instance, #4447 is now printed:
λ Ca Da : ℕAlg,
let (ℕ, ℕ0) := (Ca, Da) in
let (C, p) := ℕ in
let (c₀, cs) := p in
let (D, p0) := ℕ0 in
let (d₀, ds) := p0 in
{h : C → D & ((h c₀ = d₀) * (∀ c : C, h (cs c) = ds (h c)))%type}
: ℕAlg → ℕAlg → Type
|
|
|
|
|
|
|
|
This scheme has been advised by @gashe on #79.
Interestingly there are several comparison functions in Coq which were already implemented with this scheme.
|
|
|
|
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
|
|
|
|
|
|
|
|
We artificially restrict the syntax though, because it is unclear of
what the semantics of several axioms in a row is, in particular about the
resolution of remaining evars.
|
|
These options can be set to a string value, but also unset.
Internal data is of type string option.
|
|
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
|
|
|
|
|
|
|
|
|
|
guardedness.
|
|
Seems to be morally required since we have the -type-in-type flag.
|
|
|
|
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
