aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Expand)Author
2017-12-14Add named timers to LtacProfJason Gross
2017-10-19Moving bug numbers to BZ# format in the source code.Théo Zimmermann
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-07-05Fix typo in documentation for identityTej Chajed
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 04:27:47 +0000