aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-27minor clarifications in constrintern.ml:sort_fieldsGabriel Scherer
2016-06-27Patterns in binders: printing testsArnaud Spiwack
2016-06-27Patterns in binders: functional testsArnaud Spiwack
2016-06-27Merge branch 'funpattern' into trunk. Was PR#142: Binder syntax.Maxime Dénès
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-27More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).Hugo Herbelin
2016-06-27Fix bug #4698: CoqIDE error dialogs piling up when coqtop dies.Pierre-Marie Pédrot
2016-06-25[xmlproto] Remove duplicated deserialization.Emilio Jesus Gallego Arias
2016-06-25[doc] Update changes for feedback.Emilio Jesus Gallego Arias
2016-06-25[feedback] Remove `ErrorMsg` in favor of `Message Error`.Emilio Jesus Gallego Arias
2016-06-25[feedback] Allow messages to carry a location.Emilio Jesus Gallego Arias
2016-06-25[feedback] Add optional ?loc parameter to loggers.Emilio Jesus Gallego Arias
2016-06-25[feedback] Remove unused tag on `Debug` level.Emilio Jesus Gallego Arias
2016-06-25[merlin] Fix .merlin STM includes.Emilio Jesus Gallego Arias
2016-06-24Several easy but efficient optimizations for subst and clear tactics.Pierre-Marie Pédrot
2016-06-24Optimize the subst tactic.Pierre-Marie Pédrot
2016-06-24Optmimize the subst tactic.Pierre-Marie Pédrot
2016-06-24Optim in Clenv: use noccurn instead of depends.Pierre-Marie Pédrot
2016-06-24Optimize the subst tactic.Pierre-Marie Pédrot
2016-06-24Optimize the clear tactic.Pierre-Marie Pédrot
2016-06-24Optimize the clear tactic.Pierre-Marie Pédrot
2016-06-24Optimization in the subst tactic.Pierre-Marie Pédrot
2016-06-24Optimization in the subst tactic.Pierre-Marie Pédrot
2016-06-24Optimization in the subst tactic.Pierre-Marie Pédrot
2016-06-24Removing tactic compatibility layers in setoid_ring.Pierre-Marie Pédrot
2016-06-24Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).Hugo Herbelin
2016-06-24Makefile.install: fix a typo in last commit c954bb5, sorryPierre Letouzey
2016-06-24remove an old workaround for OCaml 3.11 + MacOS natdynlinkPierre Letouzey
2016-06-24Makefile.build: mitigate potential issues with multiple creations of pack .cmiPierre Letouzey
2016-06-24Makefile.install: fix the install of plugin cmiPierre Letouzey
2016-06-23Better algorithm for variable deambiguation in term printing.Pierre-Marie Pédrot
2016-06-23Makefile.doc: fix 'make doc'Pierre Letouzey
2016-06-23Fix typo.Guillaume Melquiond
2016-06-23Remove extraction-specific code from the checker.Guillaume Melquiond
2016-06-22Makefile.build: "make;make" should redo nothingPierre Letouzey
2016-06-21Makefile: compat5* moved in grammar/, less -I given to camlp4oPierre Letouzey
2016-06-21Parsing/compat.ml4: avoid "let open" syntax, unsupported by my camlp5 6.11Pierre Letouzey
2016-06-20Merge remote-tracking branch 'github/pr/212' into trunkMaxime Dénès
2016-06-20Reference Manual / Extraction: the original example command no longer works w...Matej Kosik
2016-06-20Add file name, line number and beginning of line position to locations.Maxime Dénès
2016-06-20LtacProf reports structured results (pr/209)CJ Bell
2016-06-20COMMENTS: Vernacexpr.extend_nameMatej Kosik
2016-06-20Small optimization in clear_body.Pierre-Marie Pédrot
2016-06-20Fix bug #4825: [clear] should not dependency-check hypotheses that come above...Pierre-Marie Pédrot
2016-06-20Prevent a useless evar normalization in Clenvtac.unify.Pierre-Marie Pédrot
2016-06-20Do not evar-normalize goals when interpreting some hardwired genargs.Pierre-Marie Pédrot
2016-06-19Add [Unset Printing Dependent Evars Line]Jason Gross
2016-06-19Merge 'pr/215' into trunkEnrico Tassi
2016-06-19Fix bug #4836: Anomaly: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
2016-06-18Fix path separator on windowsJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 08:23:35 +0000