| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Still unsure about .o file (should they be shipped for the native_compute
machinery or .cmxs suffice?)
|
|
|
|
|
|
the import of goal.ml and, afaiu, ocaml does not provide a way to
refer to a shadowed module.
|
|
|
|
full instances.
|
|
- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)
Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
|
|
in tactic unification.
|
|
|
|
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.
|
