coq - The formal proof system

Age	Commit message (Collapse)	Author
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	Merge branch 'v8.5'	Pierre-Marie Pédrot

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-10	Merge branch 'v8.5'	Pierre-Marie Pédrot

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	Merge branch 'v8.5'	Pierre-Marie Pédrot

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.