aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
* Revert "Fix Qcanon after changes on injection."Gravatar Maxime Dénès2014-05-18
* Moving argument-free tactics out of the AST into a dedicatedGravatar Pierre-Marie Pédrot2014-05-16
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Update and start testing rewrite-in-type code.Gravatar Matthieu Sozeau2014-05-09
* Restore implicit arguments of irreflexivity (fixes bug #3305).Gravatar Matthieu Sozeau2014-05-09
* Removing comment outdated since eta holds in conversion rule (thisGravatar Hugo Herbelin2014-05-07
* Fix after merge.Gravatar Matthieu Sozeau2014-05-06
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Gravatar Matthieu Sozeau2014-05-06
* Restore reasonable performance by not allocating during universe checks,Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Pos.iter arguments in a better order for cbn.Gravatar Pierre Boutillier2014-05-02
* Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentGravatar Pierre Boutillier2014-05-02
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* Fix Qcanon after changes on injection.Gravatar Maxime Dénès2014-04-30
* Import proof of decidability of negated formulas from Coquelicot.Gravatar Guillaume Melquiond2014-04-23
* Remove some uses of excluded middle.Gravatar Guillaume Melquiond2014-04-22
* Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...Gravatar Guillaume Melquiond2014-04-22
* Fixing missing headers.Gravatar Hugo Herbelin2014-04-16
* No more Coersion in Init.Gravatar Pierre Boutillier2014-04-10
* Define [projT3] and [proj3_sig]Gravatar Jason Gross2014-04-10
* Closing bug #3164Gravatar Julien Forest2014-04-04
* Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.Gravatar Guillaume Melquiond2014-03-10
* Pos.compare_cont takes the comparison as first argumentGravatar Pierre Boutillier2014-02-28
* fixup complement FinGravatar Pierre Boutillier2014-02-24
* Less dependencies in Omega.Gravatar Pierre-Marie Pédrot2014-02-08
* FinFun.v: results about injective/surjective/bijective fonctions over finite ...Gravatar Pierre Letouzey2014-02-07
* [Coercion]s use [Sortclass], not [Prop] (in docs)Gravatar Jason Gross2014-01-24
* List: Bug 3039 weaker requirement for fold symmetricGravatar Pierre Boutillier2013-12-20
* Better unification for [projT1] and [proj1_sig].Gravatar Jason Gross2013-12-12
* Generalize eq_proofs_unicityGravatar Jason Gross2013-12-12
* Improved the presentation of the proof of UIP_refl_nat.Gravatar Hugo Herbelin2013-12-04
* Add lemma derivable_pt_lim_atan.Gravatar Guillaume Melquiond2013-12-04
* Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Gravatar Guillaume Melquiond2013-12-03
* Remove a useless hypothesis from Rle_Rinv.Gravatar Guillaume Melquiond2013-12-03
* Adding Acc_intro_generator in order to help computations of Function in parti...Gravatar forest2013-11-20
* Nicer infered names in refine.Gravatar aspiwack2013-11-04
* Restore Zsqrt compat now that refine works fine with match.Gravatar aspiwack2013-11-02
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
* Side effect free implementation of admit (Isabelle's oracle)Gravatar gareuselesinge2013-08-08
* Adding a dependent version of equal_f, thus fixing #3074.Gravatar ppedrot2013-08-02
* Typo in definition clos_reflGravatar ppedrot2013-07-31
* Fixing #3089. This implied tweaking the definition of the lexicographicGravatar ppedrot2013-07-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 19:52:02 +0000