aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-08-19[pcoq] Remove unneeded casting operators.Emilio Jesus Gallego Arias
2019-08-19[parsing] Move pcoq-specific parts in extend to pcoq.Emilio Jesus Gallego Arias
2019-08-18[api] Move `Keys` to pretypingEmilio Jesus Gallego Arias
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
2019-08-16Merge PR #10663: Fix quoting in 8.9 changelog entry.Clément Pit-Claudel
2019-08-16Fix quoting in 8.9 changelog entry.Théo Zimmermann
2019-08-16Fix typing_flags in the checkerSimonBoulier
2019-08-16Fix Print Assumptions: Inductive types can have unsafe fixpoints orSimonBoulier
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add documentation for typing flags.SimonBoulier
2019-08-16Add a file for typing_flags in the test-suite.SimonBoulier
2019-08-16Improve [Print Assumptions] for type-in-type and assumed positive.SimonBoulier
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-08-16Add [Print Typing Flags] command.SimonBoulier
2019-08-16Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...SimonBoulier
2019-08-16Apply suggestions from code reviewOliver Nash
2019-08-16New lemmas for List.vOliver Nash
2019-08-16Merge PR #10457: Make rewrite use the registered elimination schemesPierre-Marie Pédrot
2019-08-14[vernac] Refactor common parts of interp_{,delayed}Emilio Jesus Gallego Arias
2019-08-14[vernac] Pass control attributes to interpretation of delayed proofs.Emilio Jesus Gallego Arias
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
2019-08-14Merge PR #10642: Emit Feedback.AddedAxiom in Declare instead of higher layersPierre-Marie Pédrot
2019-08-10[extraction] Fix #7191: Avoid unsound eta-reductionKazuhiko Sakaguchi
2019-08-10Compute (if linear_order_T 0 (IPR 22) (IPR 10) (IPR_pos 10) then true else fa...Vincent Semeria
2019-08-10Make rewrite use the registered elimination schemesAndreas Lynge
2019-08-09Switch constructive Rlt to sort Type, to make it compute laterVincent Semeria
2019-08-09Add a changelog entryKazuhiko Sakaguchi
2019-08-09Overlay for #10642Gaëtan Gilbert
2019-08-09Recommend assigning an issue before fixing a bug.Théo Zimmermann
2019-08-09Merge PR #10641: Fix regression of #10637 (-emacs arg should set color to `EM...Emilio Jesus Gallego Arias
2019-08-08Emit Feedback.AddedAxiom in Declare instead of higher layersGaëtan Gilbert
2019-08-08Merge PR #10639: map directory read error to empty directoryEmilio Jesus Gallego Arias
2019-08-08Fix regression of #10637 (-emacs arg sets color to `EMACS)Jim Fehrle
2019-08-08Fix namespace of Cauchy realsVincent Semeria
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
2019-08-08Add interface of constructive real numbers, with an opaque implementation by ...Vincent Semeria
2019-08-08map directory read error to empty directoryspanjel
2019-08-08[doc][ssr][under][setoid] Add changelog entryErik Martin-Dorel
2019-08-08[ssr] under: Add a contrived example to test under/over with SetoidsErik Martin-Dorel
2019-08-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
2019-08-07[funind] Move some exception-based control flow to explicit option typing.Emilio Jesus Gallego Arias
2019-08-07[funind] Port indfun to the new tactic engine.Emilio Jesus Gallego Arias
2019-08-07Merge PR #10604: Simplify Lib section handlingEmilio Jesus Gallego Arias
2019-08-07Merge PR #10525: [funind] Miscellaneous code reorganizations and cleanupPierre-Marie Pédrot
2019-08-06Prove the completeness of real numbers from logical axiom sig_not_decVincent Semeria
2019-08-06[parsing] unify checks for contiguity of tokens in Ltac2 and G_primEnrico Tassi
2019-08-06[ssr] under: extend ssreflect.v to generalize iff to any setoid eqErik Martin-Dorel
2019-08-06[ssr] export Ssrequality.ssr_is_setoidErik Martin-Dorel
2019-08-06Merge PR #10557: Fixing #10286 (coqide hangs on invalid filenames)Pierre-Marie Pédrot
2019-08-06Merge PR #10618: Add missing *.exe files to "make clean"Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-04 12:26:41 +0000