index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2017-04-25
[toplevel] Use exception information for error printing.
Emilio Jesus Gallego Arias
2017-04-25
[located] [doc] Improve docs for `CAst.ast`.
Emilio Jesus Gallego Arias
2017-04-25
Fix an optimization failure in tclPROGRESS.
Pierre-Marie Pédrot
2017-04-25
Fix an optimization failure in tclPROGRESS.
Pierre-Marie Pédrot
2017-04-25
Merge PR#567: Fix bug #5377: @? patterns broken.
Maxime Dénès
2017-04-25
Merge PR#578: Fix nsatz not recognizing real literals.
Maxime Dénès
2017-04-25
[travis] mathcomp and fiat overlay for #402
Emilio Jesus Gallego Arias
2017-04-25
[location] Cleanup.
Emilio Jesus Gallego Arias
2017-04-25
[location] [ast] Port module AST to CAst
Emilio Jesus Gallego Arias
2017-04-25
[location] [ast] Switch Constrexpr AST to an extensible node type.
Emilio Jesus Gallego Arias
2017-04-25
[location] Be consistent with type module qualification
Emilio Jesus Gallego Arias
2017-04-25
[location] Document changes.
Emilio Jesus Gallego Arias
2017-04-25
[location] Remove `Loc.internal_ghost`
Emilio Jesus Gallego Arias
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-24
[location] Use located in tactics.
Emilio Jesus Gallego Arias
2017-04-24
[location] Use located in misctypes.
Emilio Jesus Gallego Arias
2017-04-24
[location] More located use.
Emilio Jesus Gallego Arias
2017-04-24
[location] Switch glob_constr to Loc.located
Emilio Jesus Gallego Arias
2017-04-24
[location] Move Glob_term.predicate_pattern to located.
Emilio Jesus Gallego Arias
2017-04-24
[location] Move Glob_term.cases_pattern to located.
Emilio Jesus Gallego Arias
2017-04-24
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-24
[constrexpr] Make patterns use Loc.located for location information
Emilio Jesus Gallego Arias
2017-04-24
[toplevel] Don't check proofs in -quick mode.
Emilio Jesus Gallego Arias
2017-04-24
[toplevel] Don't mask critical exceptions in vernac interpretation.
Emilio Jesus Gallego Arias
2017-04-24
Adding a dedicated travis overlay for fiat-parsers.
Pierre-Marie Pédrot
2017-04-24
Removing various tactic compatibility layers in core tactics.
Pierre-Marie Pédrot
2017-04-24
Porting the firstorder plugin to the new tactic API.
Pierre-Marie Pédrot
2017-04-24
Removing compatibility layer in Leminv.
Pierre-Marie Pédrot
2017-04-24
Removing tactic compatibility layer in Command.
Pierre-Marie Pédrot
2017-04-24
Removing tactic compatibility layer in congruence.
Pierre-Marie Pédrot
2017-04-24
Removing tactic compatibility layer in Micromega.
Pierre-Marie Pédrot
2017-04-24
Fix the API of the new pf_constr_of_global.
Pierre-Marie Pédrot
2017-04-24
Removing trivial compatibility layer in refl_omega.
Pierre-Marie Pédrot
2017-04-24
Porting omega to the new tactic API.
Pierre-Marie Pédrot
2017-04-24
Removing trivial compatibility layer in omega.
Pierre-Marie Pédrot
2017-04-24
Porting generalize_dep to the new tactic engine.
Pierre-Marie Pédrot
2017-04-24
Removing the tclWEAK_PROGRESS tactical.
Pierre-Marie Pédrot
2017-04-24
Removing the tclNOTSAMEGOAL primitive from the API.
Pierre-Marie Pédrot
2017-04-24
Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.
Maxime Dénès
2017-04-24
refman: remember the old name of template polymorphism.
Gaetan Gilbert
2017-04-24
Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.
Maxime Dénès
2017-04-24
Merge PR#552: Miscelaneous commits
Maxime Dénès
2017-04-24
Merge PR#577: Add bedrock targets src and facade to Travis CI
Maxime Dénès
2017-04-24
Merge PR#569: Documenting EConstr for developpers.
Maxime Dénès
2017-04-24
Merge PR#565: Remove VernacError
Maxime Dénès
2017-04-24
Merge PR#580: [ide] Fix #5482 "location for query commands" in IDE.
Maxime Dénès
2017-04-24
Merge PR#581: [toplevel] [emacs] Don't quote errors in emacs mode.
Maxime Dénès
2017-04-24
Merge PR#492: [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3
Maxime Dénès
2017-04-24
Merge PR#576: [ide] Rely less on `Stateid.dummy`
Maxime Dénès
[prev]
[next]