aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-05-29tactics cleanup: remove constr_of_global callsMatthieu Sozeau
2017-05-29Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Pierre Letouzey
2017-05-29Merge PR#690: [stm] Uniformize `Sideff / Sideff.Maxime Dénès
2017-05-29Ltac cleanup: no more constr_of_global callsMatthieu Sozeau
2017-05-29Equality cleanup: remove constr_of_globalMatthieu Sozeau
2017-05-29Command.ml cleanup: remove constr_of_global callsMatthieu Sozeau
2017-05-29Merge PR#555: Missing optimization when Kernel Term Sharing is disabled.Maxime Dénès
2017-05-29Configuration with -local definitively seen as an installation layout like ot...Hugo Herbelin
2017-05-29Using the same strategy in coqdoc than in coqtop to guess the coqlib.Hugo Herbelin
2017-05-29Relying on computation done in Envars to discover the installation directories.Hugo Herbelin
2017-05-29Generalizing to docdir and datadir the test for a relocated installation.Hugo Herbelin
2017-05-29Exporting the suffixes needed to build coqlib, docdir, etc.Hugo Herbelin
2017-05-29Using Coq_config.local rather than None to tell that Coq_config.coqlib is local.Hugo Herbelin
2017-05-29Cleanup: removal of constr_of_global.Matthieu Sozeau
2017-05-29Configure: viewing compilation in -local itself as an installation layout.Hugo Herbelin
2017-05-29Configuration: always giving a value to configdir and datadir.Hugo Herbelin
2017-05-29More structure and more code factorization in building defaultHugo Herbelin
2017-05-29Unifying the layout of installation directories.Hugo Herbelin
2017-05-29Unified terminology in configure.ml/coq_config.ml: arch_win32 -> arch_is_win32.Hugo Herbelin
2017-05-29Mini-renaming in configure.ml to avoid switching back and forth fromHugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 07:41:50 +0000