| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-19 | Test for #4372 (anomaly in inversion in the presence of fake dependency). | Hugo Herbelin | |
| 2015-10-19 | Turning anomaly into error for #4372 (weakness of inversion in the | Hugo Herbelin | |
| presence of dependent types with only superficial dependency). See discussion at https://coq.inria.fr/bugs/show_bug.cgi?id=4372. | |||
| 2015-10-19 | Partly fixes #3225. Removed some old experimental stuff in funind. | Pierre Courtieu | |
| 2015-10-19 | Fixed #4274, bad formatting of messages in emacs mode. | Pierre Courtieu | |
| 2015-10-19 | Documenting the option "Strict Universe Declaration" in CHANGES. | Pierre-Marie Pédrot | |
| 2015-10-18 | Miscellaneous typos, spacing, US spelling in comments or variable names. | Hugo Herbelin | |
| 2015-10-18 | Using "__" rather than this unelegant arbitrary "A" for the name of ↵ | Hugo Herbelin | |
| variables of the context of an evar in debugging mode. | |||
| 2015-10-18 | Reference Manual: Applying standard style recommendation about not | Hugo Herbelin | |
| starting a sentence with a symbolic expression. | |||
| 2015-10-18 | Fixing #4198 (continued): not matching within the inner lambdas/let-ins | Hugo Herbelin | |
| of the return clause and of the branches (what assumed that the implementation preserves the invariant that the return predicate and the branches are in canonical [fun Δ => t] form, with Δ possibly containing let-ins). | |||
| 2015-10-18 | Using appropriate lambda decomposition function counting let-ins when | Hugo Herbelin | |
| dealing with "match". Contrastingly, "fix" is considered not to count let-ins for finding the recursive argument (which is ok because the last argument is necessarily a lambda). | |||
| 2015-10-18 | Adding a function to mirror decompose_prod_n_assum in that it counts let-ins, | Hugo Herbelin | |
| to compensate decompose_lam_n_assum which does not count let-ins. Any idea on a uniform and clear naming scheme for this kind of decomposition functions? | |||
| 2015-10-17 | Lemmas accept the Local flag. | Pierre-Marie Pédrot | |
| This was a trivial overlook. | |||
| 2015-10-17 | Test for bug #4325. | Pierre-Marie Pédrot | |
| 2015-10-16 | Generalize fix for auto from PMP to eauto and typeclasses eauto. | Matthieu Sozeau | |
| 2015-10-16 | Remove left2right reference from the kernel. | Maxime Dénès | |
| Was introduced by seemingly unrelated commit fd62149f9bf40b3f309ebbfd7497ef7c185436d5. The currently policy is to avoid exposing global references in the kernel interface when easily doable. | |||
| 2015-10-16 | Merge hint lists instead of appending them. (Fix bug #3199) | Guillaume Melquiond | |
| 2015-10-15 | Avoid dependency of the pretyper on C code. | Maxime Dénès | |
| Using the same hack as in the kernel: VM conversion is a reference to a function, updated when modules using C code are actually linked. This hack should one day go away, but always linking C code may produce some other trouble (with the OCaml debugger for instance), so better be safe for now. | |||
| 2015-10-15 | Test file for #4346: Set is no longer of type Type | Maxime Dénès | |
| 2015-10-15 | Fix #4346 2/2: VM casts were not inferring universe constraints. | Maxime Dénès | |
| 2015-10-15 | Fix #4346 1/2: native casts were not inferring universe constraints. | Maxime Dénès | |
| 2015-10-15 | Warn user when bytecode compilation fails. | Maxime Dénès | |
| Previously, the kernel was silently switching back to the standard conversion. | |||
| 2015-10-15 | Remove now useless exception handler in default conversion. | Maxime Dénès | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |