aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-04-07Inline the only use of hcons_j in Term_typing.Pierre-Marie Pédrot
2017-04-06Merge PR#455: Farewell decl_modeMaxime Dénès
2017-04-06Merge PR#488: Adding a documentation for the new proof engine.Maxime Dénès
2017-04-06Adding a documentation for the new proof engine.Pierre-Marie Pédrot
2017-04-06Documenting the fact terms are only hashconsed outside of a section.Pierre-Marie Pédrot
2017-04-06Merge PR#508: Optimize pending evarsMaxime Dénès
2017-04-06Fix a normalization hotspot in computation of constr keys.Pierre-Marie Pédrot
2017-04-06Factor interp_instance out of Pretyping.pretype_globalGaetan Gilbert
2017-04-06Avoid strange shadowing of Pretyping.interp_universe_level_nameGaetan Gilbert
2017-04-06Fix a few programming pearls related to Time, Fail and Redirect.Maxime Dénès
2017-04-06Merge PR#542: [travis] Add webhook to Gitter.Maxime Dénès
2017-04-06[travis] Add webhook to Gitter.Théo Zimmermann
2017-04-06Merge branch 'origin/v8.5' into v8.6.Hugo Herbelin
2017-04-05[toplevel] Remove exception error printer in favor of feedback printer.Emilio Jesus Gallego Arias
2017-04-05Removing a normalization hotspot from EConstr.Pierre-Marie Pédrot
2017-04-05Fixing #5454 (an assert false with 'pat).Hugo Herbelin
2017-04-05Merge PR#434: Optimizing array mapping in the kernel.Maxime Dénès
2017-04-04closing bug file for #4306Julien Forest
2017-04-04end of correction of bug 4306Julien Forest
2017-04-04Bad correction in previous commitJulien Forest
2017-04-04Solving first problem in bug #4306. TO DO : solve the let in problemJulien Forest
2017-04-04bug file for 4306Julien Forest
2017-04-04Adding tests for chained abstract tactics.Pierre-Marie Pédrot
2017-04-04Fix substitution of abstracted lemmas.Pierre-Marie Pédrot
2017-04-04Merge PR#502: [pp] Add anomaly header to error messages.Maxime Dénès
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-04-04Merge PR#535: Fix #5435: [Eval native_compute in] raises anomaly.Maxime Dénès
2017-04-04Test file for #5435: [Eval native_compute in] raises anomaly.Maxime Dénès
2017-04-04Fix bug #5435: [Eval native_compute in] raises anomaly.Maxime Dénès
2017-04-03Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-03Merge PR#533: Instances should obey universe binders even when defined by tac...Maxime Dénès
2017-04-03Fix loading of ocamldebug printers.Pierre-Marie Pédrot
2017-04-03Instances should obey universe binders even when defined by tactics.Gaetan Gilbert
2017-04-03Merge PR#417: No cast surgery in let inMaxime Dénès
2017-04-03Add test file for #4957.Maxime Dénès
2017-04-02Fix higher-order pattern variables not being printed as "@?" (bug #5431).Guillaume Melquiond
2017-04-02Fix documentation typo (bug #5433).Guillaume Melquiond
2017-04-02Simplify some proofs.Guillaume Melquiond
2017-04-01Restore a fast path in EConstr instance normalization.Pierre-Marie Pédrot
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-04-01Declaring ltac plugin, so that static linking works.Hugo Herbelin
2017-04-01Actually exporting delayed universes in the EConstr implementation.Pierre-Marie Pédrot
2017-03-31Make the Constr.kind_of_term type parametric in sorts and universes.Pierre-Marie Pédrot
2017-03-31Ensuring proper cast invariants in EConstr.kind.Pierre-Marie Pédrot
2017-03-31Revert "Specially crafted EConstr.kind to be more efficient."Pierre-Marie Pédrot
2017-03-30Specially crafted EConstr.kind to be more efficient.Pierre-Marie Pédrot
2017-03-30Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-30Merge PR#463: Run non-tactic comands without resilient_commandMaxime Dénès
2017-03-30Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Guillaume Melquiond
2017-03-30Merge PR#469: Added take to VectorDefMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 11:56:47 +0000