aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Expand)Author
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2017-05-11Merge PR#201: Transparent abstractMaxime Dénès
2017-05-05Merge PR#605: Report a useful error for dependent inductionMaxime Dénès
2017-05-05Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteMaxime Dénès
2017-05-03Report a useful error for dependent inductionTej Chajed
2017-04-30Functional choice <-> [inhabited] and [forall] commuteGaetan Gilbert
2017-04-28Add .dir-locals.el and _CoqProject files for emacs stdlib editingJason Gross
2017-04-27Merge PR#584: Give andb_prop a simpler proofMaxime Dénès
2017-04-26Small typo in commentVadim Zaliva
2017-04-25Add transparent_abstract tacticJason Gross
2017-04-25Give andb_prop a simpler proofJason Gross
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-06Merge PR#455: Farewell decl_modeMaxime Dénès
2017-04-06Merge branch 'origin/v8.5' into v8.6.Hugo Herbelin
2017-03-17Merge PR#442: Allow interactive editing of Coq.Init.LogicMaxime Dénès
2017-03-17Merge PR#451: Add η principles for sigma typesMaxime Dénès
2017-03-07Farewell decl_modeEnrico Tassi
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-01Add η principles for sigma typesJason Gross
2017-03-01Remove some trailing whitespace in Init/Specif.vJason Gross
2017-02-23Fixing a little bug in printing ex2 (type was printed "_" by default).Hugo Herbelin
2017-02-21Allow interactive editing of Coq.Init.LogicJason Gross
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-07-18Replacing deprecated Implicit Arguments in prelude.Maxime Dénès
2016-07-18Remove the swap tactic from the prelude.Maxime Dénès
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-16Adding option "Set Reversible Pattern Implicit" to Specif.v so that anHugo Herbelin
2016-04-27Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"Hugo Herbelin
2016-04-27Adding option "Set Reversible Pattern Implicit" to Specif.v so that anHugo Herbelin
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-03-06Moving Eauto to a simple ML file.Pierre-Marie Pédrot
2016-02-23Moving tauto.ml4 to a proper ML file.Pierre-Marie Pédrot
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2015-10-02Remove Print Universe directive.Matthieu Sozeau
2015-10-02Universes: enforce Set <= i for all Type occurrences.Matthieu Sozeau
2015-08-14Move type_scope into user space, fix some output logsJason Gross
2015-08-14Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Jason Gross
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Adding a notation { x & P } for { x : _ & P }.Hugo Herbelin
2015-05-09Tentatively setting cons and Some with 1st implicit argument maximalHugo Herbelin
2015-03-31Fix various typos in documentationMatěj Grabovský
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-25Reorder the steps of the easy tactic. (Fix for bug #2630)Guillaume Melquiond
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-06 10:27:50 +0000