| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-01-15 | Remove left-over dead code in previous commit. | Maxime Dénès | |
| 2015-01-15 | Make -print-mod-uid accept a list of files. | Maxime Dénès | |
| Solves an efficiency problem in Makefiles generated by coq_makefile. | |||
| 2015-01-15 | Mention CHANGES file in COMPATIBILITY. | Maxime Dénès | |
| 2015-01-15 | Mention guard condition in CHANGES. | Maxime Dénès | |
| 2015-01-15 | Make installation of native files more robust. | Maxime Dénès | |
| 2015-01-15 | Mention CHANGES file in COMPATIBILITY. | Maxime Dénès | |
| 2015-01-15 | Mention guard condition in CHANGES. | Maxime Dénès | |
| 2015-01-15 | Make installation of native files more robust. | Maxime Dénès | |
| 2015-01-15 | Hugo put me in credits, but I was already there :) | Maxime Dénès | |
| 2015-01-15 | Makefile: install ide/*lang | Enrico Tassi | |
| 2015-01-15 | coq_makefile: chmod 755 on toplopp cmxs | Enrico Tassi | |
| 2015-01-15 | CoqIDE: a Make file to build coqidetop toploop | Enrico Tassi | |
| 2015-01-15 | coq_makefile installs native files | Pierre Boutillier | |
| 2015-01-15 | Always build (even when -coqide no) and install idetoploop | Pierre Boutillier | |
| So you can link a coqtop compiled (by opam) without coqide to a stand alone coqide (binary distributed) | |||
| 2015-01-15 | Hugo put me in credits, but I was already there :) | Maxime Dénès | |
| 2015-01-15 | Tentatively updating credits while remaining brief. | Hugo Herbelin | |
| 2015-01-14 | Makefile: install ide/*lang | Enrico Tassi | |
| 2015-01-14 | coq_makefile: chmod 755 on toplopp cmxs | Enrico Tassi | |
| 2015-01-14 | CoqIDE: a Make file to build coqidetop toploop | Enrico Tassi | |
| 2015-01-14 | Reference manual: I had previously omitted the syntax entry for [> t1|…|tn]. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document tryif/then/else. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document multimatch. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: try and improve documentation for Ltac's match. | Arnaud Spiwack | |
| In particular document the "once" behaviour. | |||
| 2015-01-14 | Reference manual: try and improve the documentation of lazymatch. | Arnaud Spiwack | |
| In particular try to avoid the use of the word "backtracking" which refers to too many things. | |||
| 2015-01-14 | Reference manual: document gfail. | Arnaud Spiwack | |
| 2015-01-14 | CHANGES: my recent updates to Ltac. | Arnaud Spiwack | |
| - gfail - multimatch - tryif/then/else | |||
| 2015-01-14 | Reference manual: I had previously omitted the syntax entry for [> t1|…|tn]. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document tryif/then/else. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: document multimatch. | Arnaud Spiwack | |
| 2015-01-14 | Reference manual: try and improve documentation for Ltac's match. | Arnaud Spiwack | |
| In particular document the "once" behaviour. | |||
| 2015-01-14 | Reference manual: try and improve the documentation of lazymatch. | Arnaud Spiwack | |
| In particular try to avoid the use of the word "backtracking" which refers to too many things. | |||
| 2015-01-14 | Reference manual: document gfail. | Arnaud Spiwack | |
| 2015-01-14 | CHANGES: my recent updates to Ltac. | Arnaud Spiwack | |
| - gfail - multimatch - tryif/then/else | |||
| 2015-01-14 | coq_makefile installs native files | Pierre Boutillier | |
| 2015-01-14 | Always build (even when -coqide no) and install idetoploop | Pierre Boutillier | |
| So you can link a coqtop compiled (by opam) without coqide to a stand alone coqide (binary distributed) | |||
| 2015-01-13 | Bump version and magic numbers in configure. | Maxime Dénès | |
| 2015-01-13 | Tentatively updating credits while remaining brief. | Hugo Herbelin | |
| 2015-01-13 | Made -print-mod-uid more silent and robust. | Maxime Dénès | |
| This is a follow-up on Pierre's 5d80a385. | |||
| 2015-01-13 | Refresh some copyright headers. | Maxime Dénès | |
| 2015-01-13 | Native compiler: if debug flag not present, remove .native files. | Maxime Dénès | |
| 2015-01-13 | More documentation of the Local Definitions and Axioms. | Pierre-Marie Pédrot | |
| 2015-01-13 | More in CHANGES about local definitions | Pierre-Marie Pédrot | |
| 2015-01-13 | TCs: Properly handle Hint Extern with conclusions of the form _ -> _ | Matthieu Sozeau | |
| in typeclasses eauto, remaining compatible with eauto and still producing eta-reduced applications for Hint Resolves. Fixes bug #3794. | |||
| 2015-01-13 | Fix test-suite file, we were testing that no anomaly was raised | Matthieu Sozeau | |
| and this is the case now. | |||
| 2015-01-13 | Update hash of cic.mli in checker/values.ml, | Matthieu Sozeau | |
| letting make validate progress. | |||
| 2015-01-13 | Fix bug when discharging universe constraints coming from variables | Matthieu Sozeau | |
| into monomorphic constants, which was still using the de Bruijn encoding Bug revealed by discharging of hidden internal monomorphic definition in otherwise polymorphic developments. Makes coqchk work on Hurkens again. | |||
| 2015-01-13 | Fix issue in printing due to de Bruijn bug when constructing compatibility | Matthieu Sozeau | |
| constr for primitive records (not used anywhere else than printing). Problem reported by P. LeFanu Lumsdaine on HoTT/HoTT. Also add some minor fixes in detyping and pretty printing related to universes. | |||
| 2015-01-12 | typo in coqide compilation rules after -thread requirement | Pierre Boutillier | |
| 2015-01-12 | Derive -> derive occurences | Pierre Boutillier | |
| 2015-01-12 | Coq_makefile erases native compiler files | Pierre Boutillier | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |