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-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-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-05Merge PR#434: Optimizing array mapping in the kernel.Maxime Dénès
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-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
2017-03-30Added take to VectorDef.George Stelle
2017-03-30Merge PR#511: [stm] Remove some obsolete vernacs/classification.Maxime Dénès
2017-03-29Merge PR#522: [coqide] Protect against size_allocate race in proofview.Maxime Dénès
2017-03-29Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-29Merge PR#514: [travis] Backport from trunk: VSTMaxime Dénès
2017-03-29Merge PR#506: [nit] Fix a couple incorrect uses of msg_error.Maxime Dénès
2017-03-29Merge PR#521: Do so that "About" tells if a reference is a coercion.Maxime Dénès
2017-03-29Merge PR#525: [ide] Fix typo in pp serialization.Maxime Dénès
2017-03-29Merge branch 'trunk' into pr379Maxime Dénès
2017-03-29Fix call to broken unsafe_type_of in apply tactic.Maxime Dénès
2017-03-29Run non-tactic comands without resilient_commandTej Chajed
2017-03-29[ide] Fix typo in pp serialization.Emilio Jesus Gallego Arias
2017-03-28Revert to incorrect heuristic in apply.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 03:26:12 +0000