aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-10-18Constraining refine to monotonic functions.Pierre-Marie Pédrot
2015-10-18Adding a notion of monotonous evarmap.Pierre-Marie Pédrot
2015-10-17Clarifying and documenting the UState API.Pierre-Marie Pédrot
2015-10-17Dedicated file for universe unification context manipulation.Pierre-Marie Pédrot
This allows to remove a lot of independent code from Evd which was put into the UState module. The API is not perfect yet, but this is a first pass. Names of data structures should be thought about too because they are way too similar.
2015-10-16Merge branch 'v8.5' into trunkMaxime Dénès
2015-10-16Hashcons bytecode generated by the VM.Pierre-Marie Pédrot
2015-10-16Exporting a purely functional interface to bytecode patching.Pierre-Marie Pédrot
2015-10-16Remove 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-16Merge hint lists instead of appending them. (Fix bug #3199)Guillaume Melquiond
2015-10-15Avoid 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-15Test file for #4346: Set is no longer of type TypeMaxime Dénès
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
Previously, the kernel was silently switching back to the standard conversion.
2015-10-15Remove now useless exception handler in default conversion.Maxime Dénès
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-15Fix 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-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
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-14Fix LemmaOverloadingMatthieu 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-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
failing for unresolved evars (regression).
2015-10-14Univs: inductives, remove unneeded testMatthieu Sozeau
2015-10-14Temporary 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-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
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-14Remove unused infos structure in VM.Maxime Dénès
Became unused after c47b205206d832430fa80a3386be80149e281d33.
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-12Merge branch 'v8.5'Pierre-Marie Pédrot
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
direct aliases are ok, and indices should not be made polymorphic. Fixes NFix.
2015-10-12Fix Definition id := Eval <redexpr> in by passing the right universeMatthieu Sozeau
context to the reduction function. Fixes MapleMode.
2015-10-12Fix rechecking of applications: it can be given ill-typed terms. Fixes ↵Matthieu Sozeau
math-classes.
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
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-11Refining 0c320e79ba30 in fixing interpretation of constr under bindersHugo 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 03:13:05 +0000