aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2017-03-28Fixing missing PropFacts.v in Logic/vo.itarget.Hugo Herbelin
2017-03-28[readme] Add badges for Travis and Gitter.Emilio Jesus Gallego Arias
2017-03-28[coqide] Protect against size_allocate race in proofview.Emilio Jesus Gallego Arias
2017-03-27Do so that "About" tells if a reference is a coercion.Hugo Herbelin
2017-03-27More efficient check in validity of side-effects.Pierre-Marie Pédrot
2017-03-27Adding the size of the opaquetab in its representation.Pierre-Marie Pédrot
2017-03-27Fix hashconsing of terms in the kernel.Pierre-Marie Pédrot
2017-03-25Mathcomp overlay.Maxime Dénès
2017-03-24Fix interpretation of Ltac patterns episode 2.Maxime Dénès
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24[travis] Backport from trunk: VSTEmilio Jesus Gallego Arias
2017-03-24Merge PR#489: [travis] Add VSTMaxime Dénès
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
2017-03-24[nit] Fix a couple incorrect uses of msg_error.Emilio Jesus Gallego Arias
2017-03-24[travis] Add VSTEmilio Jesus Gallego Arias
2017-03-24Applying same convention as in Definition for printing type in a let in.Hugo Herbelin
2017-03-24Applying same convention as in Definition for parsing type in a let in.Hugo Herbelin
2017-03-24Documenting main changes of API.Hugo Herbelin
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-03-24Using the same type of binders for interning and externing.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-26 00:23:28 +0000