aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-05-04labelizing argumentsPierre Courtieu
2017-05-04Adding an option "Printing Unfocused".Pierre Courtieu
2017-05-03Generalizing the tactic-in-term embedding to any generic argument.Pierre-Marie Pédrot
2017-05-03Generalizing the refine primitive so as to accept tactic arguments.Pierre-Marie Pédrot
2017-05-03Allowing to pass arbitrary data in internalization environments.Pierre-Marie Pédrot
2017-05-03Exporting Nametab generic API.Pierre-Marie Pédrot
2017-05-03FIx bug #5300: uncaught exception in "Print Assumptions".Cyprien Mangin
2017-05-03Merge PR#541: Fixing "decide equality" bug #5449Maxime Dénès
2017-05-03Merge PR#588: Allow interactive editing of {C,}Morphisms in PGMaxime Dénès
2017-05-03Merge PR#386: Better editing of the standard library in coqtop/PGMaxime Dénès
2017-05-03Make congruence reuse discriminate instead of rolling its own.Gaetan Gilbert
2017-05-03Merge PR#602: Fix more warningsMaxime Dénès
2017-05-03Merge PR#404: patch for printing types of let bindingsMaxime Dénès
2017-05-03Merge PR#603: Fix outdated description in RefMan.Maxime Dénès
2017-05-03Adding an even more compact mode for goal display.Pierre Courtieu
2017-05-03Added an option Set Debug Cbv.Hugo Herbelin
2017-05-03Report a useful error for dependent inductionTej Chajed
2017-05-03Reorganize comment documentation of ChoiceFacts.vGaetan Gilbert
2017-05-03Type@{_} should not produce a flexible algebraic universe.Gaetan Gilbert
2017-05-03Allow flexible anonymous universes in instances and sorts.Gaetan Gilbert
2017-05-03Merge PR#411: Mention template polymorphism in the documentation.Maxime Dénès
2017-05-03Fix outdated description in RefMan.Théo Zimmermann
2017-05-02applied the patch for printing types of let bindings by @herbelinAbhishek Anand (@brixpro-home)
2017-05-02Remove dead code in native compiler.Maxime Dénès
2017-05-02Fix two new unused opens.Maxime Dénès
2017-05-02Remove unused module definition after merging PR#592.Maxime Dénès
2017-05-02Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto.Maxime Dénès
2017-05-02Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with...Maxime Dénès
2017-05-02Merge PR#582: Fix warningsMaxime Dénès
2017-05-02Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite filesMaxime Dénès
2017-05-02Merge PR#599: Repairing `Set Rewriting Schemes`Maxime Dénès
2017-05-02Merge PR#596: Fix for bug 5507. Mispelt de Bruijn.Maxime Dénès
2017-05-02Avoiding registering files from _build_ci when not calling Makefile.ci.Hugo Herbelin
2017-05-02Merge PR#595: Avoiding registering files from _build_ci for computing depende...Maxime Dénès
2017-05-01Add bmsherman/topology to the ciJason Gross
2017-05-01Fixing Set Rewriting Schemes bugs introduced in v8.5.Hugo Herbelin
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
2017-05-01remove unneeded -emacs flag to coq-prog-argsPaul Steckler
2017-05-01Removing dead code in Autorewrite.Pierre-Marie Pédrot
2017-05-01Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Hugo Herbelin
2017-05-01Really fixing #2602 which was wrongly working because of #5487 hiding the cause.Hugo Herbelin
2017-05-01Fix for bug 5507. Mispelt de Bruijn.Théo Zimmermann
2017-05-01Avoiding registering files from _build_ci when not calling Makefile.ci.Hugo Herbelin
2017-05-01Answer to db28e827d: I did test the commit on test-suite but for someHugo Herbelin
2017-04-30Functional choice <-> [inhabited] and [forall] commuteGaetan Gilbert
2017-04-30Fix bug #5501: Universe polymorphism breaks proof involving auto.Pierre-Marie Pédrot
2017-04-30Fixing "decide equality"'s bug #5449.Hugo Herbelin
2017-04-29Suppress warning message in stdlib.Guillaume Melquiond
2017-04-28Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."Maxime Dénès
2017-04-28Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 18:32:03 +0000