coq - The formal proof system

Age	Commit message (Collapse)	Author
2014-04-09	Fix exponential behavior in native compiler with retroknowledge.	Maxime Dénès

2014-04-09	Optimizing Int31 support in native compiler, by not tagging	Maxime Dénès
	applications of I31 constructor as lazy.
2014-04-09	Int31 decompilation in native compiler was still partial. Now fixed.	Maxime Dénès

2014-04-09	Machine arithmetic operations for native compiler.	Maxime Dénès
	This completes the port of the native compiler to retroknowledge. However, some testing and optimizations are still to be done.
2014-04-09	Full support for int31 values in native compiler.	Maxime Dénès

2014-04-09	Partial support for open terms in int31.	Maxime Dénès

2014-04-09	Had to split Nativelambda in two files because of Retroknowledge	Maxime Dénès
	dependencies.
2014-04-09	Int31 literals in native compiler.	Maxime Dénès

2014-03-03	Fixing generic hashes and replacing them with proper ones.	Pierre-Marie Pédrot

2014-02-26	Lazyconstr -> Opaqueproof	Enrico Tassi
	Make this module deal only with opaque proofs. Make discharging/substitution invariant more explicit via a third constructor.
2013-12-30	Support for evars and metas in native compiler.	Maxime Dénès
	Experimental. Turned out to be much harder to implement than I thought. The main issue is that the reification in the native compiler and the VM is not quite untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence, when reifying an application u = t a1 ... an, the type of t has to be known or reconstructed. It is always possible to do so in plain CIC, when u is in normal form and its type is known. However, with partial terms this may no longer be the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of evars and metas. This still has to be tested more extensively, but the correction of the kernel native conversion (on terms without evars or metas) should not be impacted. Much of this could be reused for the VM.
2013-12-29	Got rid of unused lazy flag in the native compiler.	Maxime Dénès

2013-12-28	Removing native_name reference from constant_body.	Maxime Dénès
	For now, this reference (renamed to link_info) has been moved to the environment (for constants and inductive types). But this is only a first step towards making the native compiler more functional.
2013-07-06	Fixing a bug in the native compiler, introduced by r16363, leading to undefined	mdenes
	variables in the generated code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16619 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-25	Native compiler: hash-consing of generated code and values.	mdenes
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16363 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12	invalid_arg instead of raise (Invalid_argement ...)	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-05	More monomorphization.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-26	kernel/declarations becomes a pure mli	letouzey
	- constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml - the functions that were in declarations.ml (mostly substitution utilities and hashcons) are now in kernel/declareops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-11	Fixing bug in native compiler with let patterns in fixpoint definitions.	mdenes
	Typical example: Fixpoint f (m : nat) (o := true) (n : nat) {struct n} := n. Was raising an "index out of bounds" exception at compile-time. Nota: this construction is still incorrectly handled by the VM. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16197 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22	New implementation of the conversion test, using normalization by evaluation to	mdenes
	native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7