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
...
*
|
|
|
|
|
Updating .gitignore.
Pierre-Marie Pédrot
2016-03-28
*
|
|
|
|
|
Fixing an evar leak in Rewrite introduced by 968dfdb15.
Pierre-Marie Pédrot
2016-03-28
*
|
|
|
|
|
Was too restrictive in syntactic definitions, not imagining that they
Hugo Herbelin
2016-03-28
|
*
|
|
|
|
Univs: fix get_current_context (bug #4603, part I)
Matthieu Sozeau
2016-03-25
*
|
|
|
|
|
Moving back some tactics not essentially related to Ltac into the tactics/ fo...
Pierre-Marie Pédrot
2016-03-25
|
\
\
\
\
\
\
|
*
|
|
|
|
|
Moving Autorewrite back to tactics/.
Pierre-Marie Pédrot
2016-03-25
|
*
|
|
|
|
|
Making Autorewrite independent from Ltac.
Pierre-Marie Pédrot
2016-03-25
|
*
|
|
|
|
|
Moving Eqdecide to tactics/.
Pierre-Marie Pédrot
2016-03-25
|
*
|
|
|
|
|
Making Eqdecide independent of Extratactics.
Pierre-Marie Pédrot
2016-03-25
|
*
|
|
|
|
|
Moving Eauto and Class_tactics to tactics/.
Pierre-Marie Pédrot
2016-03-25
|
*
|
|
|
|
|
Moving type_uconstr to Pretyping.
Pierre-Marie Pédrot
2016-03-25
|
/
/
/
/
/
/
*
|
|
|
|
|
Test suite file for a bug in BigQ arithmetic fixed a while ago.
Maxime Dénès
2016-03-25
*
|
|
|
|
|
Test suite file for a bug in int31 arithmetic fixed a while ago.
Maxime Dénès
2016-03-25
*
|
|
|
|
|
Remove int64 emulation in bytecode interpreter.
Maxime Dénès
2016-03-25
|
*
|
|
|
|
Fix a bug in Program coercion code
Matthieu Sozeau
2016-03-25
|
*
|
|
|
|
Fix handling of arity of definitional classes.
Matthieu Sozeau
2016-03-24
|
*
|
|
|
|
use printf instead of sequenced calls to print.
Gregory Malecha
2016-03-24
|
*
|
|
|
|
add a .merlin target to the makefile
Gregory Malecha
2016-03-24
|
*
|
|
|
|
Revert "refine: do check all unif problems are solved (Close: #4415, #4532)"
Enrico Tassi
2016-03-23
|
*
|
|
|
|
refine: do check all unif problems are solved (Close: #4415, #4532)
Enrico Tassi
2016-03-23
|
*
|
|
|
|
A patch renaming equal into eq in the module dealing with
Hugo Herbelin
2016-03-22
|
*
|
|
|
|
Adding eq/compare/hash for syntactic view at
Hugo Herbelin
2016-03-22
*
|
|
|
|
|
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21
*
|
|
|
|
|
Moving the last parts of the Ltac engine to hightactics.
Pierre-Marie Pédrot
2016-03-21
|
\
\
\
\
\
\
|
*
|
|
|
|
|
Moving Tacsubst to hightactics.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Relying on generic arguments to represent Extern hints.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Adding a new Ltac generic argument for forced tactics returing unit.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Moving Tacenv to Hightactics.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Moving Tactic_debug to Hightactic.
Pierre-Marie Pédrot
2016-03-20
|
/
/
/
/
/
/
*
|
|
|
|
|
Moving the lowest parts of pretyping/ (Evarutil & Proofview) to engine/.
Pierre-Marie Pédrot
2016-03-20
|
\
\
\
\
\
\
|
*
|
|
|
|
|
Documenting changes.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Moving Evarutil and Proofview to engine/
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Making Evarutil independent from Reductionops.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Splitting Evarutil in two distinct files.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Pushing Proofview further down the dependency alley.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Moving Proofview to pretyping/.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Moving Refine to its proper module.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Making Proofview independent of Logic.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Making Proofview independent from Goal.
Pierre-Marie Pédrot
2016-03-20
|
/
/
/
/
/
/
*
|
|
|
|
|
Extruding the code for the Existential command from Proofview.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-20
|
\
|
|
|
|
|
*
|
|
|
|
|
Fixing the classification of Tactic Notation.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.
Pierre-Marie Pédrot
2016-03-20
*
|
|
|
|
|
Moving most of Ltac code to Hightactics.
Pierre-Marie Pédrot
2016-03-20
|
\
\
\
\
\
\
|
*
|
|
|
|
|
Moving Tacintern to Hightactics.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Moving the Ltac definition command to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Moving the tactic related code from Metasyntax to a new file.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Moving Print Ltac to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Moving Tactic Notation to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
|
*
|
|
|
|
|
Moving Tacinterp to Hightactics.
Pierre-Marie Pédrot
2016-03-20
[prev]
[next]
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Maxime Dénès
Matthieu Sozeau
Gregory Malecha
Enrico Tassi