| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Continuing the interface cleanup we place `Constrexpr` in the
internalization module, which is the one that eliminates it.
This slims down `pretyping` considerably, including removing the
`Univdecls` module which existed only due to bad dependency ordering
in the first place. Thanks to @ Skyskimmer we also remove a duplicate
`univ_decl` definition among `Misctypes` and `UState`.
This is mostly a proof of concept yet as it depends on quite a few
patches of the tree. For sure some tweaks will be necessary, but it
should be good for review now.
IMO the tree is now in a state where we can could easy eliminate more
than 10 modules without any impact, IMHO this is a net saving API-wise
and would help people to understand the structure of the code better.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.
With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.
|
| |
|
|
|
| |
This now works not only for parsing of fun/forall (as in 8.6), but
also for arbitraty notations with binders and for printing.
|
| |
|
|
|
|
|
|
|
| |
For instance, the following is now possible:
Check {(x,y)|x+y=0}.
Some questions remains. Maybe, by consistency, the notation should be
"{'(x,y)|x+y=0}"...
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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`.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The type `raw_cases_pattern_expr` is used only in the interpretation
of notation patterns. Indeed, this should be a private type thus we
make it local to `Constrintern`; it makes no sense to expose it in the
public AST.
The patch is routine, except for the case used to interpret primitives
in patterns. We now return a `glob_constr` representing the raw
pattern, instead of the private raw pattern type. This could be
further refactored but have opted to be conservative here.
This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754
, see the commentaries there for more information about
`raw_cases_pattern_expr`.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| | |
| |
| |
| | |
Now it is a private field, locations are optional.
|
| |/
|
|
|
|
|
|
|
| |
This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.
Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
|
| |\
| |
| |
| | |
record fields.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.
There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
explicitly asked so.
See discussion at PR #417 for more information.
|
| | |
| |
| |
| | |
This is a bit long, but it is to keep a symmetry with constr_expr.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Note: This reveals a little bug yet to fix in g_vernac.ml4. In
Definition f '((x,y):id nat * id nat) '((x',y'):id nat * id nat) := Eval unfold id in x+y = x'+y'.
the "id" are wrongly unfolded and in
Definition f '(x,y) '(x',y') := x+y = x'+y' : Prop.
an unexpected cast remains in the body of f.
|
| |/
|
|
|
|
|
|
|
|
|
|
| |
Deprecating abstract_constr_expr in favor of mkCLambdaN,
prod_constr_expr in favor of mkCProdN.
Note: They did not do exactly the same, the first ones were
interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones
were preserving the original sharing of the type, what I think is the
correct thing to do.
So, there is also a "fix" of semantic here.
|
| |
|
|
|
|
|
|
|
| |
I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.
This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.
|
| |
|
|
|
|
|
|
|
| |
The new name makes it more obvious what is meant here by "kind". We leave
Decl_kinds.binding_kind as a deprecated alias for plugin
compatibility.
We also replace bool with implicit_status in a few places in the
codebase.
|
| |
|
|
| |
Cf CHANGES for details.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
|
| |
|
|
|
| |
NB: new file miscprint.ml deserves to be part of printing.cma,
but should be part of proofs.cma for the moment, due to use in logic.ml
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
some cleaning of the interface and moving of code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16066 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
First Notations, syntactic definitions, primitive entries are tackled to build
raw_cases_pattern_expr. Reference are revolved at this time too. Then raw_patterns
are internalized as cases_pattern or applied inductive (dealing with implicit
args, or_pattern refactoring, aliases).
It is more uniform, it allows notations for non fully applied constructors but :
- It does not raise a warning when an identifier is also a global_reference
different than a constructor.
- It looks for implicit arguments twice. (because finding scopes of arguments
asks for implicit arguments).
- It does not deal anymore with constants that evaluates to constructor. (This one
is voluntary, dealing with implicit & notations is already a hell full of bugs
so what will be next step ? Any terms that computes to a pattern ???)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15439 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15382 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Maxime Dénès
Emilio Jesus Gallego Arias
Théo Zimmermann
Hugo Herbelin
Tony Beta Lambda
Pierre-Marie Pédrot
Daniel de Rauglaudre
Pierre Letouzey
ppedrot
herbelin
pboutill
letouzey