aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-10-29Removing dead code.Hugo Herbelin
2016-10-29Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).Hugo Herbelin
2016-10-29Documenting changes in typeclassesMatthieu Sozeau
2016-10-29Fixing #5164 (regression in locating error in argument of "refine").Hugo Herbelin
2016-10-28Merge remote-tracking branch 'github/pr/321' into v8.6Maxime Dénès
2016-10-28Merge remote-tracking branch 'github/pr/319' into v8.6Maxime Dénès
2016-10-28Merge commit 'fccbd64' into v8.6Maxime Dénès
2016-10-28[build] Add a target to install the META file.Emilio Jesus Gallego Arias
2016-10-28[build] META file to enable plugin linking with ocamlfind.Emilio Jesus Gallego Arias
2016-10-28Merge remote-tracking branch 'github/pr/337' into v8.6Maxime Dénès
2016-10-27Fixing #5161 (case of a notation with unability to detect a recursive binder).Hugo Herbelin
2016-10-27COMMENT: unfortunatelly, ocamldoc does not recognize this kind of markup: it ...Matej Kosik
2016-10-27Add missing dot to impargs error message.Maxime Dénès
2016-10-27Proper fix for #3753 (anomaly with implicit arguments and renamings)Maxime Dénès
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-26Using msg_info for info_auto and info_eauto (PR #324).Hugo Herbelin
2016-10-26STM: make ~valid state id non optional from APIsEnrico Tassi
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-26COMMENT: Namegen.next_ident_awayMatej Kosik
2016-10-26COMMENT: Declarations.constant_defMatej Kosik
2016-10-26COMMENT: Names.Cmap and Names.Cmap_envMatej Kosik
2016-10-26COMMENT: Proofview.entryMatej Kosik
2016-10-26COMMENT: Constr.kind_of_termMatej Kosik
2016-10-25Merge remote-tracking branch 'github/pr/338' into v8.5Maxime Dénès
2016-10-25Remove warning now that info_auto is fixed.Théo Zimmermann
2016-10-25Remove v62 from the refman.Théo Zimmermann
2016-10-25Remove v62 from the codebase.Théo Zimmermann
2016-10-25Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Maxime Dénès
2016-10-25Merge commit 'a799600' into v8.6Maxime Dénès
2016-10-25That Function is unable to create a Fixpoint equation is a user problem,Yves Bertot
2016-10-25Update CHANGES.Maxime Dénès
2016-10-25Bump version number to 8.5pl3.Maxime Dénès
2016-10-25Merge remote-tracking branch 'github/pr/333' into v8.5Maxime Dénès
2016-10-25Merge remote-tracking branch 'github/pr/329' into v8.5Maxime Dénès
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-24Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-24Adding a test for #4398 (interpretation scopes for "match goal").Hugo Herbelin
2016-10-24Rename lia.cache into .lia.cache in the test-suite Makefile.Maxime Dénès
2016-10-24Merge commit '81bdc22' into v8.6Maxime Dénès
2016-10-24Merge remote-tracking branch 'github/pr/326' into v8.5Maxime Dénès
2016-10-24Test file for #5127: Memory corruption with the VMMaxime Dénès
2016-10-24Fix #5127 Memory corruption with the VMMaxime Dénès
2016-10-24Merge branch 'v8.5' into v8.6Hugo Herbelin
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-10-24ssrmatching: fix interpretation of rpatternEnrico Tassi
2016-10-24Fixing a location bug with "?" and "$".Hugo Herbelin
2016-10-24Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{" or "}").Hugo Herbelin
2016-10-24Update .gitignore with new names for psatz cachesJason Gross
2016-10-24Fix printing of typeclasses eauto debug wrt intro.Théo Zimmermann
2016-10-24Fix 6d5fe92e to #5150 (missing dependencies in test suite) was a bit too strong.Hugo Herbelin