| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-15 | Fix detection of ties in oracle_order. | Guillaume Melquiond | |
| This commit has no impact, since l2r is always false in practice due to the definition of default_conv. | |||
| 2015-10-14 | Reverting modifications in dev/top_printers pushed mistakenly. | Pierre-Marie Pédrot | |
| 2015-10-14 | Fixing perfomance issue of auto hints induced by universes. | Pierre-Marie Pédrot | |
| Instead of brutally merging the whole evarmap coming from the clenv, we remember the context associated to the hint and we only merge that tiny part of constraints. We need to be careful for polymorphic hints though, as we have to refresh them beforehand. | |||
| 2015-10-14 | Fix LemmaOverloading | Matthieu Sozeau | |
| Do not normalize the type of a proof according to the final universes when keep_body_ucst_separate is true, otherwise the type might not be retypable in the initial context... | |||
| 2015-10-14 | Occur-check in evar_define was not strong enough. | Matthieu Sozeau | |
| 2015-10-14 | Fix constr_matching when a match is found in the head of a case construct | Matthieu Sozeau | |
| 2015-10-14 | When typechecking a lemma statement, try to resolve typeclasses before | Matthieu Sozeau | |
| failing for unresolved evars (regression). | |||
| 2015-10-14 | Univs: inductives, remove unneeded test | Matthieu Sozeau | |
| 2015-10-14 | Temporary fix: kernel conversion needs to ignore l2r flag. | Maxime Dénès | |
| Stdlib does not compile when l2r flag is actually taken into account. We should investigate... | |||
| 2015-10-14 | Exporting the original unprocessed hint in the hint running function. | Pierre-Marie Pédrot | |
| 2015-10-14 | Fixing evarmap implementation. | Pierre-Marie Pédrot | |
| 2015-10-14 | Remove reference to default conversion function inside the kernel. | Maxime Dénès | |
| 2015-10-14 | Remove -vm flag of coqtop. | Maxime Dénès | |
| Used to replace the standard conversion by the VM. Not so useful, and implemented using a bunch of references inside and outside the kernel. | |||
| 2015-10-14 | Remove unused infos structure in VM. | Maxime Dénès | |
| Became unused after c47b205206d832430fa80a3386be80149e281d33. | |||
| 2015-10-14 | Fixing bug #4367: Wrong error message in unification. | Pierre-Marie Pédrot | |
| 2015-10-14 | Make interpreter of PROJ simpler by not using the stack. | Guillaume Melquiond | |
| 2015-10-14 | Remove some unused variables. | Guillaume Melquiond | |
| 2015-10-14 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-12 | Remove code that was already commented out. | Maxime Dénès | |
| 2015-10-12 | Univs: be more restrictive for template polymorphic constants: only | Matthieu Sozeau | |
| direct aliases are ok, and indices should not be made polymorphic. Fixes NFix. | |||
| 2015-10-12 | Fix Definition id := Eval <redexpr> in by passing the right universe | Matthieu Sozeau | |
| context to the reduction function. Fixes MapleMode. | |||
| 2015-10-12 | Fix rechecking of applications: it can be given ill-typed terms. Fixes ↵ | Matthieu Sozeau | |
| math-classes. | |||
| 2015-10-12 | Gather VM tags in Cbytecodes. | Maxime Dénès | |
| 2015-10-11 | Adding test for bug #4366. | Pierre-Marie Pédrot | |
| 2015-10-11 | Fixing bug #4366: Conversion tactics recheck uselessly convertibility. | Pierre-Marie Pédrot | |
| 2015-10-11 | Fixing test-suite | Hugo Herbelin | |
| 2015-10-11 | Documenting matching under binders. | Hugo Herbelin | |
| 2015-10-11 | Fixing untimely unexpected warning "Collision between bound variables" (#4317). | Hugo Herbelin | |
| Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables. | |||
| 2015-10-11 | Refining 0c320e79ba30 in fixing interpretation of constr under binders | Hugo Herbelin | |
| which was broken after it became possible to have binding names themselves bound to ltac variables (2fcc458af16b). Interpretation was corrected, but error message was damaged. | |||
| 2015-10-11 | Fixing obviously untested fold_glob_constr and iter_glob_constr. | Hugo Herbelin | |
| 2015-10-11 | Constr_matching: renaming misleading name stk into ctx. | Hugo Herbelin | |
| 2015-10-10 | Fix a few latex errors in documentation of Proof Using (e.g. \tt*). | Guillaume Melquiond | |
| 2015-10-09 | Complete handling of primitive projections in VM. | Maxime Dénès | |
| This commit is a follow-up to a51cce369b9c634a93120092d4c7685a242d55b1 | |||
| 2015-10-09 | Code cleaning in VM (with Benjamin). | Maxime Dénès | |
| Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values. | |||
| 2015-10-09 | Minor typo in universe polymorphism doc. | Maxime Dénès | |
| 2015-10-09 | Refine fix for handling of the universe contexts of hints, depending on | Matthieu Sozeau | |
| their polymorphic status _and_ locality. | |||
| 2015-10-09 | Fix CFGV contrib: handling of global hints introducing global universes. | Matthieu Sozeau | |
| It was wrong, the context was readded needlessly to the local evar_map context. | |||
| 2015-10-09 | Fix Next Obligation to not raise an anomaly in case of mutual | Matthieu Sozeau | |
| definitions. | |||
| 2015-10-09 | Fix inference of return clause raising a type error. | Matthieu Sozeau | |
| 2015-10-09 | STM: Work around an occasional crash in dot (debug output) | Alec Faithfull | |
| The splines=ortho option seems to make dot crash sometimes, so this commit removes it from the STM debugging output | |||
| 2015-10-09 | TQueue: Allow some tasks to be saved when clearing a TQueue | Alec Faithfull | |
| 2015-10-09 | TQueue: Expose the length of TQueues | Alec Faithfull | |
| 2015-10-09 | STM: Added functions for saving and restoring the internal state | Alec Faithfull | |
| PIDEtop needs these to implement its new transaction mechanism | |||
| 2015-10-09 | STM: Pass exception information to unreachable_state_hook functions | Alec Faithfull | |
| This lets hooks treat different exceptions in different ways; in particular, user interrupts can now be safely ignored | |||
| 2015-10-09 | Remove misleading warning (Close #4365) | Enrico Tassi | |
| 2015-10-08 | Univs: fix bug #3807 | Matthieu Sozeau | |
| Add a flag to disallow minimization to set | |||
| 2015-10-08 | Allowing empty bound universe variables. | Pierre-Marie Pédrot | |
| 2015-10-08 | Univs: fix bug #4161. | Matthieu Sozeau | |
| Retypecheck abstracted infered predicate to register the right universe constraints. | |||
| 2015-10-08 | Axioms now support the universe binding syntax. | Pierre-Marie Pédrot | |
| We artificially restrict the syntax though, because it is unclear of what the semantics of several axioms in a row is, in particular about the resolution of remaining evars. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |