aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-06-01Fix coq_makefile uninstall target under OSX.Maxime Dénès
2017-06-01Merge PR#694: Fixing #5523 (missing support for complex constructions in recu...Maxime Dénès
2017-06-01Break circular dependency in MExtractionJason Gross
2017-06-01a solution that works also with make 3.81Matej Kosik
2017-06-01extract "plugins/micromega/micromega.ml{,i}" files from "plugins/micromega/ME...Matej Kosik
2017-06-01[printing] Remove duplicated printing function.Emilio Jesus Gallego Arias
2017-06-01Merge PR#704: Fix empty parentheses display in test-suiteMaxime Dénès
2017-05-31Merge PR#701: [readlink -f] doesn't work on OSXMaxime Dénès
2017-05-31Reformat Makefile.ciJason Gross
2017-05-31[proof] Deprecate "proof mode" APIEmilio Jesus Gallego Arias
2017-05-31Merge PR#248: Adding eassert, eset, epose, etc.Maxime Dénès
2017-05-31Makefile.build: test-suite all = run + report, so don't report againGaëtan Gilbert
2017-05-31[travis] print failing test suite logs on failureGaëtan Gilbert
2017-05-31Tests for new specialize feature + CHANGES.Pierre Courtieu
2017-05-31Documenting the new behaviour of specialize.Pierre Courtieu
2017-05-31Make specialize smarter.Pierre Courtieu
2017-05-31Merge PR#700: make sure that "ocamllibdep" properly recognizes Ocaml that are...Maxime Dénès
2017-05-31removing duplicate line from "tools/CoqMakefile.in"Matej Košík
2017-05-31Adding overlay for math-comp.Hugo Herbelin
2017-05-31Using a more explicit algebraic type for evars of kind "MatchingVar".Hugo Herbelin
2017-05-31Renaming allow_patvar flag of intern_gen into pattern_mode.Hugo Herbelin
2017-05-31Overlay for math-comp.Hugo Herbelin
2017-05-31Factorizing interp_gen through a function interpreting glob_constr.Hugo Herbelin
2017-05-31Splitting interp_open_constr into two variants, with or without type classes.Hugo Herbelin
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-31Renaming interp_rawcontext_evars using a more "standard" name.Hugo Herbelin
2017-05-31Locating error about clash between a inductive parameter and a bound variable.Hugo Herbelin
2017-05-31More precise on preventing clash between bound vars name and hidden impargs.Hugo Herbelin
2017-05-31Fixing #5233 (missing implicit arguments for recursive records).Hugo Herbelin
2017-05-31Fixing a failure to interpret some local implicit arguments in Inductive.Hugo Herbelin
2017-05-31Using EConstr and more invariants in record.ml.Hugo Herbelin
2017-05-31Fixing #5523 (missing support for complex constructions in recursive notations).Hugo Herbelin
2017-05-31Fixing a too lax constraint for finding recursive binder part of a notation.Hugo Herbelin
2017-05-30[ide] Correct merging error.Emilio Jesus Gallego Arias
2017-05-30Merge PR#706: Add some test-suite generated files to .gitignoreMaxime Dénès
2017-05-30[gitlab] Artifact test suite logs on failure.Gaëtan Gilbert
2017-05-30Add some test-suite generated files to .gitignoreJason Gross
2017-05-30Fix empty parentheses display in test-suiteJason Gross
2017-05-30[readlink -f] doesn't work on OSXGaëtan Gilbert
2017-05-30Support for using type information to infer more precise evar sources.Hugo Herbelin
2017-05-30Documentation for eassert, eenough, epose proof, eset, eremember, epose.Hugo Herbelin
2017-05-30Few tests for e-variants of assert, set, remember.Hugo Herbelin
2017-05-30Adding "epose", "eset", "eremember" which allow to set terms withHugo Herbelin
2017-05-30Adding "eassert", "eenough", "epose proof", which allow to stateHugo Herbelin
2017-05-30make sure that "ocamllibdep" properly recognizes Ocaml modules that are all u...Matej Košík
2017-05-30Merge PR#356: Making management of installation directories more structured, ...Maxime Dénès
2017-05-30cleanup in ".merlin" fileMatej Kosik
2017-05-30make the expansion of the "DECLARE PLUGIN" closer to the way how a human woul...Matej Kosik
2017-05-30Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3Maxime Dénès
2017-05-29Merge PR#687: Gitlab CIMaxime Dénès