coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Making Vernacexpr independent from Tacexpr.	Pierre-Marie Pédrot	2016-09-08
\|
*	Add and document match, fix and cofix reduction flags.	Maxime Dénès	2016-07-01
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Extend the syntax of simpl with a delta flag.	Arnaud Spiwack	2014-12-12
\| \| \| \|	You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n").
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
\| \| \| \| \| \| \| \| \| \| \| \| \|	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
*	Yet a new reduction tactic in Coq : cbn	pboutill	2012-12-21
\| \| \| \| \| \| \| \| \| \| \|	It is supposed to become the next generation of the simpl tactics (it "refolds" constant) but 1/it is a bit more aggresive than the old simpl 2/it cannot be customized as simpl start to be 3/(for now)it does not refold in reccursive calls constant such as compare x y := compare_cont x y Eq := (fix compare_cont x y s := ...) x y Eq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16111 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of identifier	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
\| \| \| \| \| \| \| \| \| \|	were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29
	Stuff about reductions now in genredexpr.mli, operations in redops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7