aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Expand)Author
2017-06-13Merge PR#385: Equality of sigma typesMaxime Dénès
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2017-05-28More uniform indentation of sigma lemmasJason Gross
2017-05-28Give explicit proof terms to proj2_sig_eq etc.Jason Gross
2017-05-28Use the rew dependent notation in ex, ex2 proofsJason Gross
2017-05-28Make theorems about ex equality QedJason Gross
2017-05-28Make new proofs of equality QedJason Gross
2017-05-28Add some more comments about sigma equalitiesJason Gross
2017-05-28Remove motive argument from [rew dependent]Jason Gross
2017-05-28Use a local [rew dependent] notationJason Gross
2017-05-28Add forward-chaining versions: [eq_sig*_uncurried]Jason Gross
2017-05-28Use notation for sigTJason Gross
2017-05-28Remove reference to [IsIso]Jason Gross
2017-05-28Use notations for [sig], [sigT], [sig2], [sigT2]Jason Gross
2017-05-28Use extended notation for ex, ex2 typesJason Gross
2017-05-28Replace [ex'] with [ex]Jason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
2017-05-28Add equality lemmas for sig2 and sigT2Jason Gross
2017-05-28Add lemmas for ex2Jason Gross
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
2017-05-28Add an [inversion_sigma] tacticJason Gross
2017-05-28Add lemmas about equality of sigma typesJason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
2017-05-28Add more groupoid-like theorems about [eq]Jason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:48:54 +0000