aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-01-15Hugo put me in credits, but I was already there :)Maxime Dénès
2015-01-15Makefile: install ide/*langEnrico Tassi
2015-01-15coq_makefile: chmod 755 on toplopp cmxsEnrico Tassi
2015-01-15CoqIDE: a Make file to build coqidetop toploopEnrico Tassi
2015-01-14Reference manual: I had previously omitted the syntax entry for [> t1|…|tn].Arnaud Spiwack
2015-01-14Reference manual: document tryif/then/else.Arnaud Spiwack
2015-01-14Reference manual: document multimatch.Arnaud Spiwack
2015-01-14Reference manual: try and improve documentation for Ltac's match.Arnaud Spiwack
2015-01-14Reference manual: try and improve the documentation of lazymatch.Arnaud Spiwack
2015-01-14Reference manual: document gfail.Arnaud Spiwack
2015-01-14CHANGES: my recent updates to Ltac.Arnaud Spiwack
2015-01-14coq_makefile installs native filesPierre Boutillier
2015-01-14Always build (even when -coqide no) and install idetoploopPierre Boutillier
2015-01-13Tentatively updating credits while remaining brief.Hugo Herbelin
2015-01-13Made -print-mod-uid more silent and robust.Maxime Dénès
2015-01-13Refresh some copyright headers.Maxime Dénès
2015-01-13Native compiler: if debug flag not present, remove .native files.Maxime Dénès
2015-01-13More documentation of the Local Definitions and Axioms.Pierre-Marie Pédrot
2015-01-13More in CHANGES about local definitionsPierre-Marie Pédrot
2015-01-13TCs: Properly handle Hint Extern with conclusions of the form _ -> _Matthieu Sozeau
2015-01-13Fix test-suite file, we were testing that no anomaly was raisedMatthieu Sozeau
2015-01-13Update hash of cic.mli in checker/values.ml,Matthieu Sozeau
2015-01-13Fix bug when discharging universe constraints coming from variablesMatthieu Sozeau
2015-01-13Fix issue in printing due to de Bruijn bug when constructing compatibilityMatthieu Sozeau
2015-01-12typo in coqide compilation rules after -thread requirementPierre Boutillier
2015-01-12Derive -> derive occurencesPierre Boutillier
2015-01-12Coq_makefile erases native compiler filesPierre Boutillier
2015-01-12fixup to vi -> vio renamingEnrico Tassi
2015-01-12Whodidwhat-8.5: a global passArnaud Spiwack
2015-01-12whodidwhat-8.5: typo.Arnaud Spiwack
2015-01-12Add -no-native-compiler flag to list dumped by --help.Maxime Dénès
2015-01-12Add myself to credits.Maxime Dénès
2015-01-12Update credits.Guillaume Melquiond
2015-01-12Fix files in test-suite having to do with Require inside modules.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-12Update test for #3363 now that Require is forbidden inside modules.Maxime Dénès
2015-01-12Fix a few typos.Maxime Dénès
2015-01-12Fixing name of evars in output test Notation.v.Hugo Herbelin
2015-01-12Not "Setting ?n=?p order to ?p:=?n to see if it solves someHugo Herbelin
2015-01-12Fixing typo in previous commit.Hugo Herbelin
2015-01-11Fixing wrong duplication message when finding both a .ml and a .ml4 in coqdep.Hugo Herbelin
2015-01-11Avoiding a redundant information in unification error message.Hugo Herbelin
2015-01-11some credits for STMEnrico Tassi
2015-01-11Extraction: discard code unnecessary to fulfill a module signaturePierre Letouzey
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-11Extraction: discard unnecessary code inside modules without signaturesPierre Letouzey
2015-01-11Extraction: no more ascii blob in type variables (fix #3227)Pierre Letouzey
2015-01-11Extraction : some more support functions for a future "Extraction Compute"Pierre Letouzey
2015-01-11Extraction: minor tweaks to ease ongoing experiments about LambdaPierre Letouzey
2015-01-10Adding more sharing in Map.udpate and Map.modify.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 16:28:44 +0000