| Age | Commit message (Collapse) | Author |
|---|
|
|
|
a UserError to ease debugging.
|
|
|
|
|
|
|
|
defined and the file providing the primitives.
The datatypes are defined in [Proofview_monad], previous [Proofview_monad] is now called [Logic_monad] since it is more generic since the refactoring.
|
|
|
|
|
|
and unsatisfiable constraints which were not done in the right environment.
|
|
|
|
|
|
it became possible to have binding names themselves bound to ltac
variables (2fcc458af16b).
|
|
|
|
reorganization of apply in d5fece25d8964d5d9fcd55b66164286aeef5fb9f:
using renaming also in retyping.
|
|
|
|
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
|
|
|
Add a flag to indicate if we're in the toplevel or debuggger to not try
to retype terms in the wrong environment (and making find_rectype,
get_type_of untraceable). This fixes bug #3638 along with the previous
commit.
|
|
The official Coq logo does not work as a splash screen.
Simplest fix: no splash screen.
|
|
This makes the hammer tools/mkwinapp.ml kind of obsolete
|
|
|
|
|
|
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
|
|
|
|
|
|
|
|
For debugging purposes.
|
|
|
|
|
|
|
|
|
|
- checks for paths containing whitespaces
- Coqide has syntax highlighting
- does not include the ocaml compiler, since it would not work anyway
for the purpose of native compile. For that we really need the whole
toolchain, including the C linker/assembler. Hence we should just
recommend to install the SDK
|
|
Not 100% functional, but coqide works.
The native compiler is embedded but:
- some path mangling problem prevents it from working even when run via
cygwin (like in the build process)
- CAMLLIB must be exported to ${COQ}\ocaml\lib to have it run
(coq should do it).
fix
|
|
|
|
scheme, redundancies, possibility of chaining a tactic knowing the
name of introduced hypothesis, new proof engine).
|
|
- emphasizing the different kinds of patterns
- factorizing code of the non-naming intro-patterns
Still some questions:
- Should -> and <- apply to hypotheses or not (currently they apply to
hypotheses either when used in assert-style tactics or apply in, or
when the term to rewrite is a variable, in which case "subst" is
applied)?
- Should "subst" be used when the -> or <- rewrites an equation x=t
posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)?
- Should -> and <- be applicable in non assert-style if the lemma has
quantifications?
|
|
|
|
|
|
- realargs: refers either to the indices of an inductive, or to the proper args
of a constructor
- params: refers to parameters (which are common to inductive and constructors)
- allargs = params + realargs
- realdecls: refers to the defining context of indices or proper args
of a constructor (it includes letins)
- paramdecls: refers to the defining context of params (it includes letins)
- alldecls = paramdecls + realdecls
|
|
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/
|
|
|
|
|
|
bindings of the same variable (fixing HoTT bug #52). Document the unification
of universes in Ltac/tactics.
|
|
- Monomorphize Cst_stack to 'a = constr.
- Add corresponding debug printer.
|
|
|
|
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.
|
|
|
