aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-05-24[location] Fix warnings.Emilio Jesus Gallego Arias
2017-05-24[location] Renaming "CAst.ast" to "CAst.t"Matej Košík
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24Merge PR#642: Small cleanup on `close_proof` type.Maxime Dénès
2017-05-24Merge PR#650: Fixing an extra bug with pattern_of_constrMaxime Dénès
2017-05-24Merge PR#671: unification.mli: Fix a spelling typo in a commentMaxime Dénès
2017-05-23unification.mli: Fix a spelling typo in a commentJason Gross
2017-05-23Merge PR#661: Added a test for #4765 (an example of printing abbreviation wit...Maxime Dénès
2017-05-23Merge PR#659: Mention ./configure in INSTALL.docMaxime Dénès
2017-05-23Merge PR#657: [test-suite] Add tests for goal printing.Maxime Dénès
2017-05-23Merge PR#646: Revised behavior on ill-formed identifiersMaxime Dénès
2017-05-23Merge PR#660: Change wrong bullet message.Maxime Dénès
2017-05-23Merge PR#518: Faster universe unificationMaxime Dénès
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
2017-05-23[vernac] Remove `Save.` command.Emilio Jesus Gallego Arias
2017-05-20Added a test for #4765 (an example of printing abbreviation with binders).Hugo Herbelin
2017-05-20Deprecate -nodoc.Théo Zimmermann
2017-05-20Change wrong bullet message.Théo Zimmermann
2017-05-20Revised behavior on ill-formed identifiers.Hugo Herbelin
2017-05-20Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890).Maxime Dénès
2017-05-20Mention ./configure in INSTALL.docThéo Zimmermann
2017-05-20Merge PR#654: Travis: do not cache opam logs (+prettier spacing)Maxime Dénès
2017-05-20Merge PR#643: [ide] Disable `print_ast` call.Maxime Dénès
2017-05-20Merge PR#474: A fix for #5390 (a useful error on used introduction names was ...Maxime Dénès
2017-05-20[test-suite] Add tests for goal printing.Emilio Jesus Gallego Arias
2017-05-20Merge PR#627: Obligations shrinking: shrink abstraction tooMaxime Dénès
2017-05-20Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Maxime Dénès
2017-05-20Merge PR#648: Allow interactive editing of `plugins/` by adding .dir-locals.elMaxime Dénès
2017-05-20Merge PR#649: Fix a typoMaxime Dénès
2017-05-20Merge PR#651: Re-adding explicit dependency of misc universe test into all_st...Maxime Dénès
2017-05-20Merge PR#640: [toplevel] Restore 8.6 goal printing behavior.Maxime Dénès
2017-05-19Travis: do not cache opam logs (+prettier spacing)Gaetan Gilbert
2017-05-19Re-adding explicit dependency of misc universe test into all_stdlib.v.Hugo Herbelin
2017-05-19Fixing an extra bug with pattern_of_constr.Hugo Herbelin
2017-05-18Fix a typoJason Gross
2017-05-18Add .dir-locals.el to pluginsJason Gross
2017-05-18[toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Emilio Jesus Gallego Arias
2017-05-18[ide] Disable `print_ast` call.Emilio Jesus Gallego Arias
2017-05-17A fix for #5390 (a useful error on used introduction names was masked).Hugo Herbelin
2017-05-17Merge PR#633: An extension of EXTEND and notations to make standard parsing t...Maxime Dénès
2017-05-17Documenting relaxing of constraints on injection.Hugo Herbelin
2017-05-17Stopping injection not to work on discriminable atoms (see #4890).Hugo Herbelin
2017-05-17Merge PR#457: Adding an even more compact goal hyps mode.Maxime Dénès
2017-05-17Merge PR#607: Make congruence reuse discriminate instead of rolling its own.Maxime Dénès
2017-05-17[toplevel] Restore 8.6 goal printing behavior.Emilio Jesus Gallego Arias
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-17Merge PR#620: Reorganization of the layout for miscellaneous testsMaxime Dénès
2017-05-17Merge PR#614: Improve TravisMaxime Dénès
2017-05-17Travis: add -warn-error targets (standard and 4.04.1 ocaml)Gaetan Gilbert
2017-05-17Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanupMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 15:26:02 +0000