aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Test for #4372 (anomaly in inversion in the presence of fake dependency).Gravatar Hugo Herbelin2015-10-19
|
* Turning anomaly into error for #4372 (weakness of inversion in theGravatar Hugo Herbelin2015-10-19
| | | | | | presence of dependent types with only superficial dependency). See discussion at https://coq.inria.fr/bugs/show_bug.cgi?id=4372.
* Partly fixes #3225. Removed some old experimental stuff in funind.Gravatar Pierre Courtieu2015-10-19
|
* Fixed #4274, bad formatting of messages in emacs mode.Gravatar Pierre Courtieu2015-10-19
|
* Documenting the option "Strict Universe Declaration" in CHANGES.Gravatar Pierre-Marie Pédrot2015-10-19
|
* Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
|
* Using "__" rather than this unelegant arbitrary "A" for the name of ↵Gravatar Hugo Herbelin2015-10-18
| | | | variables of the context of an evar in debugging mode.
* Reference Manual: Applying standard style recommendation about notGravatar Hugo Herbelin2015-10-18
| | | | starting a sentence with a symbolic expression.
* Fixing #4198 (continued): not matching within the inner lambdas/let-insGravatar Hugo Herbelin2015-10-18
| | | | | | | 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).
* Using appropriate lambda decomposition function counting let-ins whenGravatar Hugo Herbelin2015-10-18
| | | | | | | | 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).
* Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,Gravatar Hugo Herbelin2015-10-18
| | | | | | | 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?
* Lemmas accept the Local flag.Gravatar Pierre-Marie Pédrot2015-10-17
| | | | This was a trivial overlook.
* Test for bug #4325.Gravatar Pierre-Marie Pédrot2015-10-17
|
* Generalize fix for auto from PMP to eauto and typeclasses eauto.Gravatar Matthieu Sozeau2015-10-16
|
* Remove left2right reference from the kernel.Gravatar Maxime Dénès2015-10-16
| | | | | | | | Was introduced by seemingly unrelated commit fd62149f9bf40b3f309ebbfd7497ef7c185436d5. The currently policy is to avoid exposing global references in the kernel interface when easily doable.
* Merge hint lists instead of appending them. (Fix bug #3199)Gravatar Guillaume Melquiond2015-10-16
|
* Avoid dependency of the pretyper on C code.Gravatar Maxime Dénès2015-10-15
| | | | | | | | | 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.
* Test file for #4346: Set is no longer of type TypeGravatar Maxime Dénès2015-10-15
|
* Fix #4346 2/2: VM casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
|
* Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
|
* Warn user when bytecode compilation fails.Gravatar Maxime Dénès2015-10-15
| | | | Previously, the kernel was silently switching back to the standard conversion.
* Remove now useless exception handler in default conversion.Gravatar Maxime Dénès2015-10-15
|
* Fix detection of ties in oracle_order.Gravatar Guillaume Melquiond2015-10-15
| | | | | This commit has no impact, since l2r is always false in practice due to the definition of default_conv.
* Reverting modifications in dev/top_printers pushed mistakenly.Gravatar Pierre-Marie Pédrot2015-10-14
|
* Fixing perfomance issue of auto hints induced by universes.Gravatar Pierre-Marie Pédrot2015-10-14
| | | | | | | 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.
* Fix LemmaOverloadingGravatar Matthieu Sozeau2015-10-14
| | | | | | 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...
* Occur-check in evar_define was not strong enough.Gravatar Matthieu Sozeau2015-10-14
|
* Fix constr_matching when a match is found in the head of a case constructGravatar Matthieu Sozeau2015-10-14
|
* When typechecking a lemma statement, try to resolve typeclasses beforeGravatar Matthieu Sozeau2015-10-14
| | | | failing for unresolved evars (regression).
* Univs: inductives, remove unneeded testGravatar Matthieu Sozeau2015-10-14
|
* Temporary fix: kernel conversion needs to ignore l2r flag.Gravatar Maxime Dénès2015-10-14
| | | | | Stdlib does not compile when l2r flag is actually taken into account. We should investigate...
* Exporting the original unprocessed hint in the hint running function.Gravatar Pierre-Marie Pédrot2015-10-14
|
* Fixing evarmap implementation.Gravatar Pierre-Marie Pédrot2015-10-14
|
* Remove reference to default conversion function inside the kernel.Gravatar Maxime Dénès2015-10-14
|
* Remove -vm flag of coqtop.Gravatar Maxime Dénès2015-10-14
| | | | | Used to replace the standard conversion by the VM. Not so useful, and implemented using a bunch of references inside and outside the kernel.
* Remove unused infos structure in VM.Gravatar Maxime Dénès2015-10-14
| | | | Became unused after c47b205206d832430fa80a3386be80149e281d33.
* Fixing bug #4367: Wrong error message in unification.Gravatar Pierre-Marie Pédrot2015-10-14
|
* Make interpreter of PROJ simpler by not using the stack.Gravatar Guillaume Melquiond2015-10-14
|
* Remove some unused variables.Gravatar Guillaume Melquiond2015-10-14
|
* Fix some typos.Gravatar Guillaume Melquiond2015-10-14
|
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
|
* Remove code that was already commented out.Gravatar Maxime Dénès2015-10-12
|
* Univs: be more restrictive for template polymorphic constants: onlyGravatar Matthieu Sozeau2015-10-12
| | | | direct aliases are ok, and indices should not be made polymorphic. Fixes NFix.
* Fix Definition id := Eval <redexpr> in by passing the right universeGravatar Matthieu Sozeau2015-10-12
| | | | context to the reduction function. Fixes MapleMode.
* Fix rechecking of applications: it can be given ill-typed terms. Fixes ↵Gravatar Matthieu Sozeau2015-10-12
| | | | math-classes.
* Gather VM tags in Cbytecodes.Gravatar Maxime Dénès2015-10-12
|
* Adding test for bug #4366.Gravatar Pierre-Marie Pédrot2015-10-11
|
* Fixing bug #4366: Conversion tactics recheck uselessly convertibility.Gravatar Pierre-Marie Pédrot2015-10-11
|
* Fixing test-suiteGravatar Hugo Herbelin2015-10-11
|
* Documenting matching under binders.Gravatar Hugo Herbelin2015-10-11
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 20:12:57 +0000