aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-06-18A cleaning phase around delayed induction arg + exporting force_induction_arg.Hugo Herbelin
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-06-17Set required version of camlp5 to 6.06.Maxime Dénès
2016-06-17par: like all: but in parallelEnrico Tassi
2016-06-17remote counter: avoid thread race on sockets (fix #4823)Enrico Tassi
2016-06-17Mentioning goal selectors in CHANGESEnrico Tassi
2016-06-16Merge branch 'nzgcd' into trunkMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 18:04:08 +0000