aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
|
* Fixing untimely unexpected warning "Collision between bound variables" (#4317).Gravatar Hugo Herbelin2015-10-11
| | | | | | 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.
* Refining 0c320e79ba30 in fixing interpretation of constr under bindersGravatar Hugo Herbelin2015-10-11
| | | | | | | 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.
* Fixing obviously untested fold_glob_constr and iter_glob_constr.Gravatar Hugo Herbelin2015-10-11
|
* Constr_matching: renaming misleading name stk into ctx.Gravatar Hugo Herbelin2015-10-11
|
* Fix a few latex errors in documentation of Proof Using (e.g. \tt*).Gravatar Guillaume Melquiond2015-10-10
|
* Complete handling of primitive projections in VM.Gravatar Maxime Dénès2015-10-09
| | | | This commit is a follow-up to a51cce369b9c634a93120092d4c7685a242d55b1
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
| | | | | Rename some functions, remove dead code related to (previously deprecated, now removed) option Set Boxed Values.
* Minor typo in universe polymorphism doc.Gravatar Maxime Dénès2015-10-09
|
* Refine fix for handling of the universe contexts of hints, depending onGravatar Matthieu Sozeau2015-10-09
| | | | their polymorphic status _and_ locality.
* Fix CFGV contrib: handling of global hints introducing global universes.Gravatar Matthieu Sozeau2015-10-09
| | | | It was wrong, the context was readded needlessly to the local evar_map context.
* Fix Next Obligation to not raise an anomaly in case of mutualGravatar Matthieu Sozeau2015-10-09
| | | | definitions.
* Fix inference of return clause raising a type error.Gravatar Matthieu Sozeau2015-10-09
|
* STM: Work around an occasional crash in dot (debug output)Gravatar Alec Faithfull2015-10-09
| | | | | The splines=ortho option seems to make dot crash sometimes, so this commit removes it from the STM debugging output
* TQueue: Allow some tasks to be saved when clearing a TQueueGravatar Alec Faithfull2015-10-09
|
* TQueue: Expose the length of TQueuesGravatar Alec Faithfull2015-10-09
|
* STM: Added functions for saving and restoring the internal stateGravatar Alec Faithfull2015-10-09
| | | | PIDEtop needs these to implement its new transaction mechanism
* STM: Pass exception information to unreachable_state_hook functionsGravatar Alec Faithfull2015-10-09
| | | | | This lets hooks treat different exceptions in different ways; in particular, user interrupts can now be safely ignored
* Remove misleading warning (Close #4365)Gravatar Enrico Tassi2015-10-09
|
* Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
| | | | Add a flag to disallow minimization to set
* Allowing empty bound universe variables.Gravatar Pierre-Marie Pédrot2015-10-08
|
* Univs: fix bug #4161.Gravatar Matthieu Sozeau2015-10-08
| | | | | Retypecheck abstracted infered predicate to register the right universe constraints.
* Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
| | | | | | 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.
* f_equal fix continued: do a refresh_universes as before.Gravatar Matthieu Sozeau2015-10-08
|
* aux_file: export API to ease writing of a Proof Using annotator.Gravatar Enrico Tassi2015-10-08
|
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
| | | | | | | | | | | | | - "Proof using p*" means: use p and any section var about p. - Simplify the grammar/parser for proof using <expression>. - Section variables with a body (let-in) are pulled in automatically since they are safe to be used (add no extra quantification) - automatic clear of "unused" section variables made optional: Set Proof Using Clear Unused. since clearing section hypotheses does not "always work" (e.g. hint databases are not really cleaned) - term_typing: trigger a "suggest proof using" message also for Let theorems.
* term_typing: strengthen discharging codeGravatar Enrico Tassi2015-10-08
| | | | | | | | | | | | | | | Given the way Lib.extract_hyps is coded if the const_hyps field of a constant declaration contains a named_context that does not have the same order of the one in Environment.env, discharging is broken (as in some section variables are not discharged). If const_hyps is computed by the kernel, then the order is correct by construction. If such list is provided by the user, the order is not granted. We now systematically sort the list of user provided section hyps. The code of Proof using is building the named_context in the right order, but the API was not enforcing/checking it. Now it does.
* CThread: blocking read + threads now worksGravatar Enrico Tassi2015-10-08
|
* Spawn: use each socket exclusively for writing or readingGravatar Enrico Tassi2015-10-08
| | | | | | According to http://caml.inria.fr/mantis/view.php?id=5325 you can't use the same socket for both writing and reading. The result is lockups (may be fixed in 4.03).
* STM: for PIDE based UIs, edit_at requires no Reach.known_stateGravatar Enrico Tassi2015-10-08
|
* Future: make not-here/not-ready messages customizableGravatar Enrico Tassi2015-10-08
|
* STM: fix backtrace handlingGravatar Enrico Tassi2015-10-08
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 23:14:14 +0000