aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-05-29Dead code (xdg_config_dirs).Hugo Herbelin
2017-05-29Merge PR#685: Fix a bug in checkerMaxime Dénès
2017-05-29Merge PR#546: Fix for bug #4499 and other minor related bugsMaxime Dénès
2017-05-29Merge PR#512: [cleanup] Unify all calls to the error function.Maxime Dénès
2017-05-28Fix a bug in checkerAmin Timany
2017-05-28Merge PR#678: [coqlib] Move `Coqlib` to `library/`.Maxime Dénès
2017-05-28Merge PR#689: Changes to make coq-makefile not failing on MacOS X.Maxime Dénès
2017-05-28Fail on deprecated warning even for Ocaml > 4.02.3Gaëtan Gilbert
2017-05-28Fixing a subtle bug in tclWITHHOLES.Hugo Herbelin
2017-05-28Merge PR#675: [coqlib] Deprecate redundant Coqlib functions.Maxime Dénès
2017-05-28Merge PR#683: coq_makefile: build .cma for each .mlpackMaxime Dénès
2017-05-28More uniform indentation of sigma lemmasJason Gross
2017-05-28Give explicit proof terms to proj2_sig_eq etc.Jason Gross
2017-05-28Use the rew dependent notation in ex, ex2 proofsJason Gross
2017-05-28Make theorems about ex equality QedJason Gross
2017-05-28Make new proofs of equality QedJason Gross
2017-05-28Add some more comments about sigma equalitiesJason Gross
2017-05-28Remove motive argument from [rew dependent]Jason Gross
2017-05-28Use a local [rew dependent] notationJason Gross
2017-05-28Add forward-chaining versions: [eq_sig*_uncurried]Jason Gross
2017-05-28Use notation for sigTJason Gross
2017-05-28Remove reference to [IsIso]Jason Gross
2017-05-28Use notations for [sig], [sigT], [sig2], [sigT2]Jason Gross
2017-05-28Use extended notation for ex, ex2 typesJason Gross
2017-05-28Replace [ex'] with [ex]Jason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
2017-05-28Add equality lemmas for sig2 and sigT2Jason Gross
2017-05-28Add lemmas for ex2Jason Gross
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
2017-05-28Add an [inversion_sigma] tacticJason Gross
2017-05-28Add lemmas about equality of sigma typesJason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
2017-05-28Add more groupoid-like theorems about [eq]Jason Gross
2017-05-28Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show MatchMaxime Dénès
2017-05-28Don't disable deprecation warning for configure.mlGaëtan Gilbert
2017-05-28Merge PR#684: Trunk+fix coq makefile test suite on nixosMaxime Dénès
2017-05-28Merge PR#681: Fix votour for safe strings & warningsMaxime Dénès
2017-05-28Gitlab CIGaëtan Gilbert
2017-05-28Merge PR#680: add Show test with -emacs flag for trunkMaxime Dénès
2017-05-28Merge PR#676: Primitive Ltac definitions for first and solveMaxime Dénès
2017-05-28Merge PR#658: [coqdoc] Add keywords in bug 2884.Maxime Dénès
2017-05-27[stm] Rename Side-Effect type.Emilio Jesus Gallego Arias
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-27[stm] Uniformize `Sideff / Sideff.Emilio Jesus Gallego Arias
2017-05-27[coqlib] Move `Coqlib` to `library/`.Emilio Jesus Gallego Arias
2017-05-27[coqlib] Deprecate redundant Coqlib functions.Emilio Jesus Gallego Arias
2017-05-27coq_makefile: build .cma for each .mlpackEnrico Tassi
2017-05-27Documenting the existence of first and solve as Ltac definitions.Pierre-Marie Pédrot
2017-05-27Exporting a few primitive tacticals as named Ltac definitions.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 08:20:35 +0000