| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
- Distinguish between primitive and non-primitive records in the kernel
declaration, so as to try eta-conversion on primitive records only.
|
| |
|
|
| |
extensions.
|
| | |
|
| |
|
|
| |
any prefix of the given qualid.
|
| |
|
|
|
|
|
|
| |
The new Term version has essentially the same behaviour as the old "Locate",
while the new raw searches for all types of objects. Also code merging with
the "Locate Ltac".
Fixes bug #3380.
|
| |
|
|
| |
command.
|
| |
|
|
|
| |
given to the obligation making function.
- Fix handling of universe context when solve_by_tac is used.
|
| |
|
|
|
|
| |
This bug was hacked around in ssreflect, but with the new idea
that parsing and interpretation are done in distinct phases the
work around could not be implemented anymore.
|
| |
|
|
| |
backtracks, print time spent in each of successive calls.
|
| |
|
|
| |
more than one constructor.
|
| | |
|
| |
|
|
| |
This is useful if a UI does not support that
|
| |
|
|
|
| |
LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- The earlier proof-of-concept file NPeano (which instantiates
the "Numbers" framework for nat) becomes now the entry point
in the Arith lib, and gets renamed PeanoNat. It still provides
an inner module "Nat" which sums up everything about type nat
(functions, predicates and properties of them).
This inner module Nat is usable as soon as you Require Import Arith,
or just Arith_base, or simply PeanoNat.
- Definitions of operations over type nat are now grouped in a new
file Init/Nat.v. This file is meant to be used without "Import",
hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
starts (but no proofs about them).
- The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
where here Nat is Init/Nat.v).
- This Coq.Init.Nat module (with only pure definitions) is Include'd
in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
sometimes instead of just Nat (for instance when doing "Print plus").
Normally it should be ok to just ignore these "Init" since
Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
it's possible to get rid of these "Init" prefixes.
- Concerning predicates, orders le and lt are still defined in Init/Peano.v,
with their notations "<=" and "<". Properties in PeanoNat.Nat directly
refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
we cannot yet include an Inductive to implement a Parameter), but these
aliased predicates won't probably be very convenient to use.
- Technical remark: I've split the previous property functor NProp in
two parts (NBasicProp and NExtraProp), it helps a lot for building
PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:
Module Nat.
Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
... (** proofs of specifications for basic ops such as + * - *)
Include NBasicProp. (** generic properties of these basic ops *)
... (** proofs of specifications for advanced ops (pow sqrt log2...)
that may rely on proofs for + * - *)
Include NExtraProp. (** all remaining properties *)
End Nat.
- All other files in directory Arith are now taking advantage of PeanoNat :
they are now filled with compatibility notations (when earlier lemmas
have exact counterpart in the Nat module) or lemmas with one-line proofs
based on the Nat module. All hints for database "arith" remain declared
in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
files are still Require'd (or not) by Arith.v, just as before.
- Compatibility should be almost complete. For instance in the stdlib,
the only adaptations were due to .ml code referring to some Coq constant
name such as Coq.Init.Peano.pred, which doesn't live well with the
new compatibility notations.
|
| |
|
|
| |
This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
|
| | |
|
| |
|
|
| |
kernel in library/universes.ml.
|
| |
|
|
|
| |
generated by a mutual inductive definition (bug found in CFGV). Actually this
code can move out of the kernel.
|
| |
|
|
|
|
| |
of the universe context in the obligations, it gets gradually fixed
globally by each one of them.
Fixes bug found in Misc/Overloading.
|
| | |
|
| | |
|
| |
|
|
|
| |
message. Otherwise, a heading space was missing when calling tclFAIL
from ML tactics.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
into a specific new cleaned file find_subterm.ml.
This makes things clearer but also solves some dependencies problem
between Evd, Termops and Pretype_errors.
|
| |
|
|
| |
proof engine. Moved it to unification.ml.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
| |
|
|
|
|
|
|
|
|
|
|
| |
User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/
and pass -toploop footop to customize the coq main loop.
A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to
functions respectively initializing the toploop (and parsing toploop
specific arguments) and running the main loop itself.
For backward compatibility -ideslave and -async-proofs worker do
set the toploop to coqidetop and stmworkertop respectively.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
for helping fixing this).
Now the issue is handled solely through refreshing of the terms assigned
to evars during unification.
If ?X = list ?Y, then Y's type is refreshed so that it doesn't mention
a template universe and in turn, ?X won't. Same goes when typechecking
(nil ?X, nil ?Y), the pair constructor levels will be set higher than fresh
universes for the lists carriers. This also handles user-defined functions
on template polymorphic inductives, which was fragile before.
Pretyping and Evd are now uncluttered from template-specific code.
|
| |
|
|
|
|
| |
and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml.
The context produced by typechecking a statement is passed in the proof, allowing the
universe name context to be correctly folded as well. Mainly an API cleanup.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
a projection constant only of the form
λ params (r : I params), match r with BuildR args => args_i end, without any
other user input and relies on it being typable (no more primitive projections
escaping this).
|
| |
|
|
| |
- Remove dead code in evarconv.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
These options no longer have any impact on the way proofs are loaded. In
other words, loading is always lazy, whatever the options. Keeping them
just so that coqc dies when the user prints some opaque symbol does not
seem worth it.
|
| |
|
|
| |
in case prefix 'e' of "apply" and co is not given.
|
| | |
|
| |
|
|
| |
- More cleanup. remove unneeded functions in universes
|
| |
|
|
|
|
|
|
| |
Universes.
Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
|
| |
|
|
| |
reduction.
|
| |
|
|
| |
the checker, and it was not used before that anyway.
|
Matthieu Sozeau
Maxime Dénès
Pierre-Marie Pédrot
Matthieu Sozeau
Enrico Tassi
Hugo Herbelin
Pierre Letouzey
Guillaume Melquiond