aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-11-23Removing a use of old refine in Tactics.Pierre-Marie Pédrot
2015-11-20Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-19Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.Pierre-Marie Pédrot
2015-11-19Allow program hooks to see the refined universe_context at the end of aMatthieu Sozeau
2015-11-19Fix bug #4433, removing hack on evars appearing in a pattern from aMatthieu Sozeau
2015-11-18Fixing fix c71aa6b to primitive projections.Hugo Herbelin
2015-11-18Fix a bug preventing the generation of graphs when doing multipleMatthieu Sozeau
2015-11-18Improve error message.Maxime Dénès
2015-11-18MacOS package script: do not fail if link to /Applications already exists.Maxime Dénès
2015-11-18Slightly documenting code for building primitive projections.Hugo Herbelin
2015-11-18Fixing logical bugs in the presence of let-ins in computiong primitiveHugo Herbelin
2015-11-18Inlining the only use of Clenv.connect_clenv.Pierre-Marie Pédrot
2015-11-17More optimizations of [Clenv.clenv_fchain].Pierre-Marie Pédrot
2015-11-17Performance fix for destruct.Pierre-Marie Pédrot
2015-11-16Being more precise and faithful about the origin of the file reportingHugo Herbelin
2015-11-15Hashconsing modules.Pierre-Marie Pédrot
2015-11-15Fixing output test Cases.v.Pierre-Marie Pédrot
2015-11-15Displaying the object identifier in votour.Pierre-Marie Pédrot
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-13Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.Matthieu Sozeau
2015-11-13MacOS package script: do not fail if directory _dmg already exists.Maxime Dénès
2015-11-12Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.Pierre-Marie Pédrot
2015-11-12Fixed test-suite file for bug #3998.Matthieu Sozeau
2015-11-12Update CHANGESJason Gross
2015-11-12Script building MacOS package.Maxime Dénès
2015-11-11Now closed.Matthieu Sozeau
2015-11-11Ensure that conversion is called on terms of the same type inMatthieu Sozeau
2015-11-11Fix bug #3998: when using typeclass resolution for conversion, allowMatthieu Sozeau
2015-11-11Fix bug #3735: interpretation of "->" in Program follows the standard one.Matthieu Sozeau
2015-11-11Fix bug #3257, setoid_reflexivity should fail if not completing the goal.Matthieu Sozeau
2015-11-11Fix bug #4293: ensure let-ins do not contain algebraic universes inMatthieu Sozeau
2015-11-11Fixing bug #3554: Anomaly: Anonymous implicit argument.Pierre-Marie Pédrot
2015-11-10Updating test-suite after Bracketing Last Introduction Pattern set byHugo Herbelin
2015-11-10Updating Compat85.v after bd1c97653 on bracketing last or-andHugo Herbelin
2015-11-10Revert "Fixing #1225: we now skip the canonically built binding contexts of"Hugo Herbelin
2015-11-10Fixing #1225: we now skip the canonically built binding contexts ofHugo Herbelin
2015-11-10Listing separately changes from 8.5betas to final 8.5 and furtherHugo Herbelin
2015-11-10Activating bracketing of last or-and introduction pattern by defaultHugo Herbelin
2015-11-10Merge origin/v8.5 into trunkHugo Herbelin
2015-11-10Dead code from the commit having introduced primitive projections (a4043608).Hugo Herbelin
2015-11-10Typo.Hugo Herbelin
2015-11-10Fixing a bug in reporting ill-formed constructor.Hugo Herbelin
2015-11-10Test for bug #4404.Pierre-Marie Pédrot
2015-11-10Fix bug #4404: [remember] gives Error: Conversion test raised an anomaly.Pierre-Marie Pédrot
2015-11-09Pushing the backtrace in conversion anomalies.Pierre-Marie Pédrot
2015-11-08Adapting output test inference.v after c23f0cab6 (experimentingHugo Herbelin
2015-11-07Fixing output test Existentials.v after eec77191b.Hugo Herbelin
2015-11-07Preventing an unwanted warning 5 "this function application is partial"Hugo Herbelin
2015-11-07Implementing assert and cut with LetIn rather than using a beta-redex.Hugo Herbelin
2015-11-07Experimenting printing the type of the defined term of a LetIn whenHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 10:43:34 +0000