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
*
Fix English spelling -> American spelling in doc.
Arnaud Spiwack
2014-08-01
*
CHANGES: [numgoals] and [guard].
Arnaud Spiwack
2014-08-01
*
Document [numgoals] and [guard].
Arnaud Spiwack
2014-08-01
*
Add [guard] tactic.
Arnaud Spiwack
2014-08-01
*
Add [numgoal] to Ltac.
Arnaud Spiwack
2014-08-01
*
Add primtive [num_goal] to Proofview.
Arnaud Spiwack
2014-08-01
*
Untyped terms in ltac: simplify [coerce_to_uconstr].
Arnaud Spiwack
2014-08-01
*
Remove spurious [1] in equality.ml.
Arnaud Spiwack
2014-08-01
*
Clean outdated comment in Proofview.Notations.
Arnaud Spiwack
2014-08-01
*
Fix typo in cf04daec997.
Arnaud Spiwack
2014-08-01
*
micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)
Frédéric Besson
2014-08-01
*
Compatibility for compilation with ocaml 3.12 (at least).
Hugo Herbelin
2014-08-01
*
micromega : improve efficiency/termination of type-checking
Frédéric Besson
2014-08-01
*
Continuing (incomplete) cleaning of Inductiveops.
Hugo Herbelin
2014-08-01
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
Removing more tactic compatibility layer.
Pierre-Marie Pédrot
2014-08-01
*
Removing some tactic compatibility layer.
Pierre-Marie Pédrot
2014-08-01
*
Useless export of Instance.eqeq. We hashcons everything before calling this
Pierre-Marie Pédrot
2014-07-31
*
Making the error message about bullets more precise.
Pierre Courtieu
2014-07-31
*
Removing the call to Weak.get_copy in hashsets.
Pierre-Marie Pédrot
2014-07-31
*
micromega : refification recognises @eq T for T convertible with Z or R
Frédéric Besson
2014-07-31
*
Typos.
Hugo Herbelin
2014-07-31
*
Finish fixes on notations and primitive projections, add test-suite files for...
Matthieu Sozeau
2014-07-31
*
Consistent pretty-printing of primitive projections and their expanded forms.
Matthieu Sozeau
2014-07-31
*
Add an option to solve typeclass goals generated by apply which can't be
Matthieu Sozeau
2014-07-31
*
Adding a generalized version of fold_Equal to FMapFacts.
Pierre Courtieu
2014-07-31
*
Optimize check of new subterm relation on match.
Maxime Dénès
2014-07-31
*
Improve intersection of regular trees.
Maxime Dénès
2014-07-31
*
Fix dynamic computation of recargs for mutual inductives.
Maxime Dénès
2014-07-31
*
Add test-suite file for bug #3439.
Matthieu Sozeau
2014-07-30
*
Avoid hconsing instances during appends and conversions from/to arrays.
Matthieu Sozeau
2014-07-30
*
Fix discrimination net which was not recognizing primitive projections.
Matthieu Sozeau
2014-07-30
*
Avoid introducing additional universes when doing pruning in evarsolve.
Matthieu Sozeau
2014-07-30
*
CHANGES: untyped terms in tactics
Arnaud Spiwack
2014-07-29
*
Document untyped terms in tactics.
Arnaud Spiwack
2014-07-29
*
Small refactoring in Ltac parsing rules.
Arnaud Spiwack
2014-07-29
*
Allow [uconstr:c] as argument of a tactic.
Arnaud Spiwack
2014-07-29
*
Untyped terms in tactic: add the possibility to use a typed term inside an un...
Arnaud Spiwack
2014-07-29
*
Untyped terms in tactic: function [type_term c] to give a typed version of [c].
Arnaud Spiwack
2014-07-29
*
Untyped term in tactics: add an grammar entry to construct them.
Arnaud Spiwack
2014-07-29
*
Add a type of untyped term to Ltac's value.
Arnaud Spiwack
2014-07-29
*
Clean up obsolete comment.
Arnaud Spiwack
2014-07-29
*
Add test-suite file for bug 3454.
Matthieu Sozeau
2014-07-29
*
Rework code for refolding projections in whd_state/whd_simpl to allow Arguments
Matthieu Sozeau
2014-07-29
*
Fix eta-conversion code which was failing in nested cases. Fixes bug #3429.
Matthieu Sozeau
2014-07-29
*
Add test-suite file for bug #3453
Matthieu Sozeau
2014-07-29
*
Fix bug #3453, not recognizing primitive projections in Coercion declarations.
Matthieu Sozeau
2014-07-29
*
Fix treatment of notations containing applications of projections (fixes bug ...
Matthieu Sozeau
2014-07-29
*
STM: print goals with no duplicates
Enrico Tassi
2014-07-29
*
Pp: only one default feedback id
Enrico Tassi
2014-07-29
[next]