aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* | | | | | Merge PR#599: Repairing `Set Rewriting Schemes`Gravatar Maxime Dénès2017-05-02
|\ \ \ \ \ \
* | | | | | | Avoiding registering files from _build_ci when not calling Makefile.ci.Gravatar Hugo Herbelin2017-05-02
| | | | * | | Add bmsherman/topology to the ciGravatar Jason Gross2017-05-01
| |_|_|/ / / |/| | | | |
| * | | | | Fixing Set Rewriting Schemes bugs introduced in v8.5.Gravatar Hugo Herbelin2017-05-01
|/ / / / /
| * | | | remove unneeded -emacs flag to coq-prog-argsGravatar Paul Steckler2017-05-01
| | * | | Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Gravatar Hugo Herbelin2017-05-01
| | * | | Really fixing #2602 which was wrongly working because of #5487 hiding the cause.Gravatar Hugo Herbelin2017-05-01
| |/ / / |/| | |
* | | | Answer to db28e827d: I did test the commit on test-suite but for someGravatar Hugo Herbelin2017-05-01
* | | | Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."Gravatar Maxime Dénès2017-04-28
|/ / /
* | | Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Gravatar Hugo Herbelin2017-04-28
* | | Merge PR#587: Fix description of command-line arguments for Add (Rec) LoadPathGravatar Maxime Dénès2017-04-27
|\ \ \
| * | | fix order of command-line arguments mentioned in Add LoadPathGravatar Paul Steckler2017-04-27
|/ / /
* | | Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.Gravatar Pierre-Marie Pédrot2017-04-27
* | | Fix an optimization failure in tclPROGRESS.Gravatar Pierre-Marie Pédrot2017-04-25
* | | Merge PR#567: Fix bug #5377: @? patterns broken.Gravatar Maxime Dénès2017-04-25
|\ \ \
* \ \ \ Merge PR#577: Add bedrock targets src and facade to Travis CIGravatar Maxime Dénès2017-04-24
|\ \ \ \
| * | | | Add bedrock targets src and facadeGravatar Jason Gross2017-04-20
|/ / / /
| * / / Fix bug #5377: @? patterns broken.Gravatar Pierre-Marie Pédrot2017-04-20
|/ / /
* | | Merge PR#538: Correction of bug #4306Gravatar Maxime Dénès2017-04-19
|\ \ \
* | | | Fixing bug #5470 (anomaly on notations with misused "binder" type).Gravatar Hugo Herbelin2017-04-14
* | | | Fixing bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-04-14
* | | | Fix EOL characters in xml protocol documentation.Gravatar Maxime Dénès2017-04-14
* | | | Merge PR#556: Fix anomaly when doing [all:Check _.] during a proof.Gravatar Maxime Dénès2017-04-14
|\ \ \ \
| * | | | Fix anomaly when doing [all:Check _.] during a proof.Gravatar Gaetan Gilbert2017-04-14
* | | | | Merge PR#563: add XML protocol doc for 8.6Gravatar Maxime Dénès2017-04-14
|\ \ \ \ \
* | | | | | [travis] Use the lite target for fiat-crypto.Gravatar Maxime Dénès2017-04-14
| |/ / / / |/| | | |
| * | | | update XML protocol doc to 8.6Gravatar Paul Steckler2017-04-13
| * | | | add XML protocol doc for 8.5Gravatar Paul Steckler2017-04-13
|/ / / /
| | | * Reinstate fixpoint refolding in [cbn], deactivated by mistake.Gravatar Matthieu Sozeau2017-04-13
| |_|/ |/| |
* | | Merge PR#510: Correctly identify [Time Defined.] as a definedGravatar Maxime Dénès2017-04-12
|\ \ \
* | | | Fixing #5460 (limitation in computing deps in pattern-matching compilation).Gravatar Hugo Herbelin2017-04-08
| | | * Better support for printing constructors with let-ins.Gravatar Hugo Herbelin2017-04-07
| | | * Fixing #4499 (not using unnamed record field in {| |} notation).Gravatar Hugo Herbelin2017-04-07
* | | | Fix a few programming pearls related to Time, Fail and Redirect.Gravatar Maxime Dénès2017-04-06
| |_|/ |/| |
* | | Merge branch 'origin/v8.5' into v8.6.Gravatar Hugo Herbelin2017-04-06
|\ \ \
* | | | Fixing #5454 (an assert false with 'pat).Gravatar Hugo Herbelin2017-04-05
| | | * closing bug file for #4306Gravatar Julien Forest2017-04-04
| | | * end of correction of bug 4306Gravatar Julien Forest2017-04-04
| | | * Bad correction in previous commitGravatar Julien Forest2017-04-04
| | | * Solving first problem in bug #4306. TO DO : solve the let in problemGravatar Julien Forest2017-04-04
| | | * bug file for 4306Gravatar Julien Forest2017-04-04
* | | | Merge PR#535: Fix #5435: [Eval native_compute in] raises anomaly.Gravatar Maxime Dénès2017-04-04
|\ \ \ \ | |_|_|/ |/| | |
| * | | Test file for #5435: [Eval native_compute in] raises anomaly.Gravatar Maxime Dénès2017-04-04
| * | | Fix bug #5435: [Eval native_compute in] raises anomaly.Gravatar Maxime Dénès2017-04-04
|/ / /
* | | Merge PR#533: Instances should obey universe binders even when defined by tac...Gravatar Maxime Dénès2017-04-03
|\ \ \
| * | | Instances should obey universe binders even when defined by tactics.Gravatar Gaetan Gilbert2017-04-03
|/ / /
* | | Add test file for #4957.Gravatar Maxime Dénès2017-04-03
* | | Merge PR#463: Run non-tactic comands without resilient_commandGravatar Maxime Dénès2017-03-30
|\ \ \
* \ \ \ Merge PR#514: [travis] Backport from trunk: VSTGravatar Maxime Dénès2017-03-29
|\ \ \ \
| | * | | Run non-tactic comands without resilient_commandGravatar Tej Chajed2017-03-29
| |/ / / |/| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 04:20:41 +0000