aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-10-15 Fix #4346 2/2: VM casts were not inferring universe constraints.Maxime Dénès
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-10-15Warn user when bytecode compilation fails.Maxime Dénès
2015-10-15Remove now useless exception handler in default conversion.Maxime Dénès
2015-10-15Fix detection of ties in oracle_order.Guillaume Melquiond
2015-10-14Reverting modifications in dev/top_printers pushed mistakenly.Pierre-Marie Pédrot
2015-10-14Fixing perfomance issue of auto hints induced by universes.Pierre-Marie Pédrot
2015-10-14Fix LemmaOverloadingMatthieu Sozeau
2015-10-14Occur-check in evar_define was not strong enough.Matthieu Sozeau
2015-10-14Fix constr_matching when a match is found in the head of a case constructMatthieu Sozeau
2015-10-14When typechecking a lemma statement, try to resolve typeclasses beforeMatthieu Sozeau
2015-10-14Univs: inductives, remove unneeded testMatthieu Sozeau
2015-10-14Temporary fix: kernel conversion needs to ignore l2r flag.Maxime Dénès
2015-10-14Exporting the original unprocessed hint in the hint running function.Pierre-Marie Pédrot
2015-10-14Fixing evarmap implementation.Pierre-Marie Pédrot
2015-10-14Remove reference to default conversion function inside the kernel.Maxime Dénès
2015-10-14Remove -vm flag of coqtop.Maxime Dénès
2015-10-14Remove unused infos structure in VM.Maxime Dénès
2015-10-14Fixing bug #4367: Wrong error message in unification.Pierre-Marie Pédrot
2015-10-14Make interpreter of PROJ simpler by not using the stack.Guillaume Melquiond
2015-10-14Remove some unused variables.Guillaume Melquiond
2015-10-14Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-12Remove code that was already commented out.Maxime Dénès
2015-10-12Univs: be more restrictive for template polymorphic constants: onlyMatthieu Sozeau
2015-10-12Fix Definition id := Eval <redexpr> in by passing the right universeMatthieu Sozeau
2015-10-12Fix rechecking of applications: it can be given ill-typed terms. Fixes math-c...Matthieu Sozeau
2015-10-12Gather VM tags in Cbytecodes.Maxime Dénès
2015-10-11Adding test for bug #4366.Pierre-Marie Pédrot
2015-10-11Fixing bug #4366: Conversion tactics recheck uselessly convertibility.Pierre-Marie Pédrot
2015-10-11Fixing test-suiteHugo Herbelin
2015-10-11Documenting matching under binders.Hugo Herbelin
2015-10-11Fixing untimely unexpected warning "Collision between bound variables" (#4317).Hugo Herbelin
2015-10-11Refining 0c320e79ba30 in fixing interpretation of constr under bindersHugo Herbelin
2015-10-11Fixing obviously untested fold_glob_constr and iter_glob_constr.Hugo Herbelin
2015-10-11Constr_matching: renaming misleading name stk into ctx.Hugo Herbelin
2015-10-10Fix a few latex errors in documentation of Proof Using (e.g. \tt*).Guillaume Melquiond
2015-10-09Complete handling of primitive projections in VM.Maxime Dénès
2015-10-09Code cleaning in VM (with Benjamin).Maxime Dénès
2015-10-09Minor typo in universe polymorphism doc.Maxime Dénès
2015-10-09Refine fix for handling of the universe contexts of hints, depending onMatthieu Sozeau
2015-10-09Fix CFGV contrib: handling of global hints introducing global universes.Matthieu Sozeau
2015-10-09Fix Next Obligation to not raise an anomaly in case of mutualMatthieu Sozeau
2015-10-09Fix inference of return clause raising a type error.Matthieu Sozeau
2015-10-09STM: Work around an occasional crash in dot (debug output)Alec Faithfull
2015-10-09TQueue: Allow some tasks to be saved when clearing a TQueueAlec Faithfull
2015-10-09TQueue: Expose the length of TQueuesAlec Faithfull
2015-10-09STM: Added functions for saving and restoring the internal stateAlec Faithfull
2015-10-09STM: Pass exception information to unreachable_state_hook functionsAlec Faithfull
2015-10-09Remove misleading warning (Close #4365)Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-24 16:24:53 +0000