aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-27minor: interp/constrintern.ml, clarify field completionGabriel Scherer
2016-06-27minor: in constrintern.ml:sort_fields, clarify sfGabriel Scherer
2016-06-27add CList.extract_firstGabriel Scherer
2016-06-27minor: in constrintern.ml:sort_fields, clarify build_pattGabriel Scherer
2016-06-27whitespace: untabity constrinternl.ml:sort_fieldsGabriel Scherer
2016-06-27minor clarifications in constrintern.ml:sort_fieldsGabriel Scherer
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-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-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-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-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
2016-06-18Fix the build on WindowsJason Gross
2016-06-18Merge PR# 169: Local type-in-type flag.Pierre-Marie Pédrot
2016-06-18Fixing the checker.Pierre-Marie Pédrot
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-18Print the type-in-type flag in various user-facing functions.Pierre-Marie Pédrot
2016-06-18Adding a local type-in-type flag in kernel declarations.Pierre-Marie Pédrot
2016-06-18Test-suite fix to 1744e37 (injection in context).Hugo Herbelin
2016-06-18Backporting c064fb933 from 8.5 (another regression with Ltac trace report).Hugo Herbelin
2016-06-18Adding an "as" clause to specialize.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:38:07 +0000