| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| | |/
|/|
| |
| | |
Universe instances were lost during constructions of the canonical instance.
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
same right-hand side.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
arguments.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.
Thanks to @SkySkimmer for lots of comments and bug-finding.
|
| | | | | | | | |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Moreover, when there are at least two clauses and the last most
factorizable one is a disjunction with no variables, turn it into a
catch-all clause.
Adding options
Unset Printing Allow Default Clause.
to deactivate the second behavior, and
Unset Printing Factorizable Match Patterns.
to deactivate the first behavior (deactivating the first one
deactivates also the second one).
E.g. printing
match x with Eq => 1 | _ => 0 end
gives
match x with
| Eq => 1
| _ => 0
end
or (with default clause deactivates):
match x with
| Eq => 1
| Lt | Gt => 0
end
More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
This is to have a better symmetry between CCases and GCases.
|
| | | | | |_|/
| | | |/| |
| | | | | |
| | | | | | |
This is a follow-up on 866b449c497933a3ab1185c194d8d33a86c432f2.
|
| | |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The exception needs to carry aroud a pair of `env, sigma` so printing
is correct. This gets rid of a few global calls, and it is IMO the
right thing to do.
While we are at it, we incorporate some fixes to a couple of
additional printing functions missing the `env, sigma` pair.
|
| | |/ / /
|/| | |
| | | |
| | | | |
And some code simplification.
|
| |\ \ \ \ |
|
| |\ \ \ \ \
| |_|_|/ /
|/| | | | |
|
| | |/ / /
|/| | | |
|
| | |/ /
|/| |
| | |
| | |
| | | |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
| | | |
| | |
| | |
| | | |
They were not used anymore since the previous patches.
|
| | | |
| | |
| | |
| | |
| | | |
This was dead code, probably due to the fact it was once shared with the
kernel stack type.
|
| |/ /
| |
| |
| |
| | |
It was actually not used. The only place generating one was easily writable
without it.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The patch has three parts:
- Introduction of a configure flag `-bytecode-compiler (yes|no)`
(due to static initialization this is a configure-time option)
- Installing the hooks that register the VM with the pretyper and the
kernel conditionally on the flag.
- Replacing the normalization function in `Redexpr` by compute if the
VM is disabled.
We also rename `Coq_config.no_native_compiler` to `native_compiler`
and `Flags.native_compiler` to `output_native_objects` [see #4607].
|
| |/
|
|
|
|
|
|
| |
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
|
| |\
| |
| |
| | |
#3125)
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
recursive functions.
|
| |\ \ |
|
| | |/
|/|
| |
| |
| | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
| | |
| |
| |
| | |
Also nicer error when the constraints are impossible.
|
| |/
|
|
| |
Before sometimes there were lists and strings.
|
| |\
| |
| |
| | |
constructs.
|
| | |
| |
| |
| |
| |
| | |
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
|
| | |
| |
| |
| | |
Note the problem with `create_evar_defs`.
|
| | |
| |
| |
| |
| |
| |
| | |
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.
|
| |\
| |
| |
| | |
unbound rel
|
| | |
| |
| |
| |
| |
| |
| | |
When an evar is undefined we need to substitute inside the evar instance.
With help from @herbelin and @psteckler to identify the issue from a
large test case.
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | |
| | | |
| | | | |
The message is the "Conversion test raised an anomaly" one.
|
| | | |/
| | |
| | |
| | | |
We do up to `Term` which is the main bulk of the changes.
|
| | |/
|/|
| |
| | |
This will allow to merge back `Names` with `API.Names`
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We refine the criterion for selecting a projection. Before PR#924 it
was alphabetic (i.e. morally "random" up to alpha-conversion). After
PR#924 it was chronological.
We refine a bit more by giving priority to simple projections when
they exist over projections which include an evar instantiation (and
which may actually be ill-typed).
|
| |/ /
| |
| |
| | |
This is a first step towards some of the solutions proposed in #6008.
|
| |\ \
| | |
| | |
| | | |
variables).
|
Maxime Dénès
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Hugo Herbelin
Théo Zimmermann
Matthieu Sozeau
Gaëtan Gilbert