| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
functionalization.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
#3125)
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We remove deprecated syntax "Coercion Local" and such, and seize the
opportunity to refactor some code around vernac_expr.
We also do a small fix on the STM classification, which didn't know about
Let Fixpoint and Let CoFixpoint.
This is a preliminary step for the work on attributes.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
|
| | |_|/
|/| |
| | |
| | |
| | | |
In particular `Proof_global.t` will become a first class object for
the upper parts of the system in a next commit.
|
| |\ \ \ |
|
| | | |/
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This function returns InProp or InSet for inductive types only when
the inductive type has been explicitly truncated to Prop or
(impredicative) Set.
For instance, singleton inductive types and small (predicative)
inductive types are not truncated and hence in Type.
|
| |\ \ \ |
|
| |\ \ \ \
| |_|_|/
|/| | | |
|
| | | | | |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | | |
In particular, we put all the context in the atts structure, and
generalize the type of the parameters of a vernac.
I hope this helps people working on "attributes", my motivation is
indeed having a more robust interpretation.
|
| | | |
| | |
| | |
| | |
| | | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
| |/ / |
|
| | |
| |
| |
| |
| |
| | |
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
|
| | |
| |
| |
| |
| |
| | |
We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
|
| | | |
|
| | |
| |
| |
| | |
Before sometimes there were lists and strings.
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | | |
This is a continuation on #6183 and another step towards a more
functional interpretation of commands.
In particular, this should allow us to remove the locality hack.
|
| | | |
| | |
| | |
| | |
| | | |
With a bit of care we can enable full deprecation warnings again in
this funny file.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
|
| | |/
|/|
| |
| |
| |
| | |
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | | |
Replaced by ident_decl in #688.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to
put any pattern in binders, prefixed by a quote."] its current
placement as well as the hook don't make a lot of sense.
In particular, they prevent parts of Coq working without linking the
parser.
To this purpose, we need to consolidate the `Constrexpr`
utilities. While we are at it we do so and remove the `Topconstr`
module which is fully redundant with `Constrexpr_ops`.
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
I followed what seems to be the intention of the code, with the
original intention of remove the global imperative proof state.
However, I fully fail to see why the new API is better than the old
one. In fact the opposite seems the contrary.
Still big parts of the "new proof engine" seem unfinished, and I'm
afraid I am not the right person to know what direction things should
take.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Due to an API change in laglgtk, we need to update CoqIDE. We use a
makefile hack so it can compile with lablgtk < 2.8.16, another option
would be to require 2.8.16 as a minimal dependency.
We also refactor travis to test more lablgtk versions.
We also need to account for improved attribute handling in 4.06.0, in
particular module aliases will propagate the deprecation status.
Fixes #6140.
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | |/
|/|
| |
| | |
We do up to `Term` which is the main bulk of the changes.
|
| |\ \
| | |
| | |
| | | |
rules
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The model provides three kinds of printers depending on whether the
printer needs a context, and, if yes if it supports levels. In the
latter case, it takes defaults levels for printing when in a
surrounded context (lconstr style) and for printing when not in a
surrounded context (constr style).
This model preserves the 8.7 focussing semantics of "idtac"
(i.e. focussing only when an env is needed) but it also shows that the
semantics of "idtac", which focusses the goal depending on the type of
its arguments, is a bit ad hoc to understand.
See discussion at PR#6047
"https://github.com/coq/coq/pull/6047#discussion_r148278454".
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| | |
We can now place most of intf modules just after `Libnames/Globnames`
which is quite low on the hierarchy.
A exception is `Vernacexpr` which still depends on `Extend` and
`GOptions`.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Originally, it was not possible to define a new vernacular command
in the following way:
VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY
[ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ]
END
because "loc : Loc.t" was not bound.
This commit fixes that, i.e. the location of the custom Vernacular command
(within *.v file) is made available as "loc" variable bound on the right side
of "->" .
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
|
| |/
|
|
|
| |
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
|
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Gaëtan Gilbert
Matej Košík