aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-03-07Merge PR#452: [ltac] Move dummy plugin to plugins folder.Maxime Dénès
2017-03-07Fixing Bug 5383 (Hyps Limit) + small refactoring.Pierre Courtieu
2017-03-07Farewell decl_modeEnrico Tassi
2017-03-07Merge PR#453: [travis] Backport trunk's travis support.Maxime Dénès
2017-03-07Merge PR#436: [ocamlbuild] Update META for the vernac split.Maxime Dénès
2017-03-06Merge PR#447: [travis] [External CI] fiat-parsersMaxime Dénès
2017-03-06Merge PR#279: A few lemmas about iff and about orders on positive and ZMaxime Dénès
2017-03-03CHANGES: choice over setoids and prop. ext.Hugo Herbelin
2017-03-03Strengthening some of the results in ChoiceFacts.v.Hugo Herbelin
2017-03-03Adding explicitly a file to work in the context of propositional extensionality.Hugo Herbelin
2017-03-03Adding a file providing extensional choice (i.e. choice over setoids).Hugo Herbelin
2017-03-03Adding various properties and characterization of the extensionalHugo Herbelin
2017-03-03Slightly unifying renaming in ChoiceFacts.v.Hugo Herbelin
2017-03-03Logic library: Adding a characterization of excluded-middle in term ofHugo Herbelin
2017-03-03Merge PR#273: Tidy stdlibMaxime Dénès
2017-03-03Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.Hugo Herbelin
2017-03-03Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.Hugo Herbelin
2017-03-03Completing "few lemmas about Zneg" with lemmas also about Zpos.Hugo Herbelin
2017-03-03A couple of other useful properties about compare_cont.Hugo Herbelin
2017-03-03Compatibility of iff wrt not and imp.Hugo Herbelin
2017-03-03Formatting references with surrounding brackets in Diaconescu.v.Hugo Herbelin
2017-03-03[ltac] Move dummy plugin to plugins folder.Emilio Jesus Gallego Arias
2017-03-02[travis] Backport trunk's travis support.Emilio Jesus Gallego Arias
2017-03-01Add η principles for sigma typesJason Gross
2017-03-01Remove some trailing whitespace in Init/Specif.vJason Gross
2017-02-27Merge PR#399: Debug by defaultMaxime Dénès
2017-02-27Merge PR#395: Allow hintdb to be parameters in a Ltac definition orMaxime Dénès
2017-02-27Do not recompute twice the whnf of terms in conversion.Pierre-Marie Pédrot
2017-02-24[travis] [External CI] fiat-parsersEmilio Jesus Gallego Arias
2017-02-24TACTIC EXTEND now takes an optional level as argument.Maxime Dénès
2017-02-24Revert "Add empty ltac_plugin file for forward compatibility."Maxime Dénès
2017-02-24Simplifying the proof of NoRetractToModalProposition.paradox inHugo Herbelin
2017-02-24Fixing anomaly on unsupported key in interactive ltac debug.Hugo Herbelin
2017-02-23Fixing a little bug in printing ex2 (type was printed "_" by default).Hugo Herbelin
2017-02-23Fixing a little bug in using the "where" clause for inductive types.Hugo Herbelin
2017-02-23Fixing #use"include" after vernac is added and ltac is moved to a plugin.Hugo Herbelin
2017-02-22Merge branch 'v8.6'Pierre-Marie Pédrot
2017-02-22Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2017-02-21Allow interactive editing of Coq.Init.LogicJason Gross
2017-02-21[travis] track an 8.7 specific branch of HoTT.Maxime Dénès
2017-02-21Merge PR#309: Ltac as a pluginMaxime Dénès
2017-02-21Add empty ltac_plugin file for forward compatibility.Maxime Dénès
2017-02-20Fix V7 syntax in refman.Théo Zimmermann
2017-02-20Deprecate -debug flag.Maxime Dénès
2017-02-20Merge PR#189: Remove tabulation support from pretty-printing.Maxime Dénès
2017-02-20Merge pull request #4 from Zimmi48/patch-1Emilio Jesús Gallego Arias
2017-02-20[ocamlbuild] fix small mistakes in descriptionsThéo Zimmermann
2017-02-20[ocamlbuild] Update meta for the vernac split.Emilio Jesus Gallego Arias
2017-02-19Fixing debugger after the split of toplevel into vernac.Pierre-Marie Pédrot
2017-02-19Optimizing array mapping in the kernel.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 22:22:48 +0000