index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Fixing strange evarmap leak in goals.
Pierre-Marie Pédrot
2014-09-18
*
For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ...
Hugo Herbelin
2014-09-18
*
mltop: when a plugin is loaded store its full path in the summary
Enrico Tassi
2014-09-18
*
Reductionops: (Co)Fixpoints are always refolded during iota
Pierre Boutillier
2014-09-18
*
fix coq_makefile
Pierre Boutillier
2014-09-18
*
configure.ml: opam camlp5 + system ocaml works
Pierre Boutillier
2014-09-18
*
seems to fix a looping coq-tex (when compiled with camlp4)
Pierre Boutillier
2014-09-18
*
Be more conservative and keep the use of eq_constr in pretyping/ functions.
Matthieu Sozeau
2014-09-17
*
Fix bug #3593, making constr_eq and progress work up to
Matthieu Sozeau
2014-09-17
*
Fix bug #3633 properly, by delaying the interpetation of constrs in
Matthieu Sozeau
2014-09-17
*
Change some Defined into Qed.
Guillaume Melquiond
2014-09-17
*
Add some missing Proof statements.
Guillaume Melquiond
2014-09-17
*
Remove pointless regex for '""' as the empty string already matches it.
Guillaume Melquiond
2014-09-17
*
Revert "coqc: execvp is now available even on win32"
Enrico Tassi
2014-09-17
*
win32: remove outdated splash screen
Enrico Tassi
2014-09-17
*
Fix highlighting of "Hint Unfold" and "Hint Rewrite".
Guillaume Melquiond
2014-09-17
*
Properly highlight the Export keyword.
Guillaume Melquiond
2014-09-17
*
Fix ambiguous regex in syntax highlighting.
Guillaume Melquiond
2014-09-17
*
Change an axiom into a definition.
Guillaume Melquiond
2014-09-17
*
Fix broken syntax highlighting for Coq files using "Proof constr".
Guillaume Melquiond
2014-09-17
*
win32: bring back the coq icon in the coqide binary
Enrico Tassi
2014-09-17
*
win32: use subsystem windows on windows (and not console)
Enrico Tassi
2014-09-17
*
Revert "While resolving typeclass evars in clenv, touch only the ones that ap...
Matthieu Sozeau
2014-09-17
*
While resolving typeclass evars in clenv, touch only the ones that appear in the
Matthieu Sozeau
2014-09-17
*
Update test-suite files after last commit. Add a file for rewrite_strat
Matthieu Sozeau
2014-09-17
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Undo prints only if coqtop || emacs
Enrico Tassi
2014-09-16
*
better error message
Enrico Tassi
2014-09-16
*
fix test-suite/success/decl_mode.v
Enrico Tassi
2014-09-16
*
More on printing references applied to implicit arguments.
Hugo Herbelin
2014-09-16
*
Add a "Hint Mode ref (+ | -)*" hint for setting a global mode
Matthieu Sozeau
2014-09-15
*
Adapting ltac output test to new interpretation of binders.
Hugo Herbelin
2014-09-15
*
Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.
Hugo Herbelin
2014-09-15
*
Not printing goal name (reinstalled by mistake in a previous commit).
Hugo Herbelin
2014-09-15
*
Fixing line break in test for #3559.
Hugo Herbelin
2014-09-15
*
Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].
Arnaud Spiwack
2014-09-15
*
Ltac names in binders: some Ltac values can be seen both as terms and identif...
Arnaud Spiwack
2014-09-15
*
Fix: when interpreting a identifier in pretying, use the Ltac identifier subs...
Arnaud Spiwack
2014-09-15
*
Fix a bug in the naming of binders.
Arnaud Spiwack
2014-09-15
*
A small pass of code cleaning and clenv removing in Rewrite.
Pierre-Marie Pédrot
2014-09-15
*
Fixing bug #3619 in emacs mode.
Hugo Herbelin
2014-09-15
*
Avoid backtracking in typeclass search if a solution for a closed
Matthieu Sozeau
2014-09-15
*
Fix bug #3610, allowing betaiotadelta reduction while unifying types of
Matthieu Sozeau
2014-09-15
*
Fix bug #3621, using fold_left2 on arrays of the same size only.
Matthieu Sozeau
2014-09-15
*
Rework typeclass resolution and control of backtracking.
Matthieu Sozeau
2014-09-15
*
Removing one Evd.merge in Rewrite.
Pierre-Marie Pédrot
2014-09-15
*
More invariants in Rewrite unification.
Pierre-Marie Pédrot
2014-09-15
*
The unifying functions of Rewrite uses the return types of strategies.
Pierre-Marie Pédrot
2014-09-15
*
Splitting the uses of the unification function according to the status of
Pierre-Marie Pédrot
2014-09-15
*
Rewrite.apply_strategy uses the same return type as strategies.
Pierre-Marie Pédrot
2014-09-14
[next]