coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Second step of integration of Program:	msozeau	2012-03-14
\| \| \| \| \| \| \| \|	- Remove useless functorization of Pretyping - Move Program coercion/cases code inside pretyping/, enabled according to a flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove support for "abstract typing constraints" that requires unicity of ↵	msozeau	2012-03-14
\| \| \| \| \| \| \| \| \| \| \|	solutions to unification. Only allow bidirectional checking of constructor applications, enabled by a program_mode flag: it is backwards-incompatible due to delta-reduction, constructor parameters might get instantiated with delta-equivalent but not syntactically equivalent terms. Prepare for merging the Program-specific version of Pretyping/Cases/Coercion with the main code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15032 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A bit of cleaning: unifying push_rels and push_rel_context.	herbelin	2012-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15031 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing vm_compute bug #2729 (function used to decompose constructors	herbelin	2012-03-13
\| \| \| \| \| \| \| \|	did not handle let-ins and was wrongly specified). Thanks to Pierre Boutillier and Pierre-Marie Pédrot for pointing out the source of the bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15027 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Univ: avoid recording dummy universe constraints u<=u or u=u	letouzey	2012-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15026 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill	2012-03-02
\| \| \| \| \| \| \| \| \|	Detyping is wrong about it and as far as I understand no one but Constrextern uses it. Constrextern has now the same machinery for all patterns. Revert if I miss something. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	"Let in" in pattern hell, one more iteration	pboutill	2012-03-02
\| \| \| \| \| \| \| \|	This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf. An other wrong externalize function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Noise for nothing	pboutill	2012-03-02
\| \| \| \| \| \| \| \| \| \| \|	Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Univ: a univ_depends function to avoid a hack in Inductiveops	letouzey	2012-03-01
\| \| \| \| \| \| \| \| \| \| \|	univ_depends checks whether a universe variable appears or is equal to a universe. In comparison with the previous hack in inductiveops based on try...catching UniverseInconsistency, this should be semantically equivalent, simplier, and more robust in case we allow someday an unsafe mode where merge_constraints would be a no-op. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15013 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Univ: a better Constraint.compare	letouzey	2012-03-01
\| \| \| \| \| \| \|	Let's gain a few % by not using Pervasive.compare on a structure containing some universe_levels, but rather UniverseLevel.compare on them. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15012 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrects the erroneous error message when trying to unfocus a fully	aspiwack	2012-03-01
\| \| \| \| \| \|	unfocused proof (part of bug #2671). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15011 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed a superfluous function in proof.mli. Preparing for incoming	aspiwack	2012-03-01
\| \| \| \| \| \|	changes of the handling of unfocusing errors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15010 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New version of recdef :	jforest	2012-03-01
\| \| \| \| \| \| \|	+ Allowing much more function to be defined. + Using completely new algorithm to define non structural fixpoints git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15009 85f007b7-540e-0410-9357-904b9bb8a0f7
*	various corrections in invfun due to a modification in induction	jforest	2012-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15008 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Univ: a faster is_leq test used when possible	letouzey	2012-02-29
\| \| \| \| \| \| \| \| \| \| \| \|	Let's reintroduce the idea of stopping the graph traversal as soon as a LE arc has been found, but this time we do so only when we're not interested by the LT/LE distinction. This way, we should remain correct but avoid largly the time penalty induced by the last fix on univ.ml: the +30% on contrib Container is almost gone, let's hope it'll be the same with Ssreflect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15007 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correcting a little bug in invfun.ml	jforest	2012-02-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction of bug 2457	jforest	2012-02-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15004 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix compilation of Constrintern...	pboutill	2012-02-29
\| \| \| \| \| \|	I love being push under presure to commit and do not try my fixup ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15003 85f007b7-540e-0410-9357-904b9bb8a0f7
*	RefMan update about match syntax.	pboutill	2012-02-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15002 85f007b7-540e-0410-9357-904b9bb8a0f7
*	In the syntax of pattern matching, the arguments of the inductive in the "in"	pboutill	2012-02-29
\| \| \| \| \| \| \| \|	clause can be any pattern. It is expanded as a match in the return clause. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15001 85f007b7-540e-0410-9357-904b9bb8a0f7
*	In the syntax of pattern matching, "in" clauses are patterns.	pboutill	2012-02-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15000 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Vector: missing injection lemmas and better impossible branches	pboutill	2012-02-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14999 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug 2703: send stdout dump to coqide when an error occurs.	pboutill	2012-02-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14998 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coq_makefile: Add of extra options by default	pboutill	2012-02-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14997 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Univ: correct compare_neq (fix #2703)	letouzey	2012-02-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	The earlier version was a bit too quick to answer <= while strict constraints could still appear from remaining universes to explore. Typical situation: compare u v when u <= v and u <= w < v. Encountering u <= v isn't enough to conclude yet... This means that kernels from r13719 to now in trunk, and from r13735 to now in 8.3 (including 8.3pl{1,2,3}) couldn't accurately detect universe inconsistencies, leading to potential proofs of False! Oups, sorry... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14993 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Implement the substitution function for global options. Fixes anomaly in ↵	msozeau	2012-02-23
\| \| \| \| \| \|	ssreflect compilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14991 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ide: sentences found by find_phrase_starting_at should be nonempty (fix #2683)	letouzey	2012-02-22
\| \| \| \| \| \| \|	In addition to #2683, this also prevent Vernac.End_of_input exceptions when a buffer ends with one of the new delimiters -+*{}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14989 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Use a heuristic to not simplify equality hypotheses remaining after ↵	msozeau	2012-02-20
\| \| \| \| \| \| \| \|	dependent induction if they don't look really trivial. We still are making a choice though. Fixes bug #2712. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14988 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- changing minimal version for OCaml: Coq uses Filename.dirsep that is ↵	notin	2012-02-20
\| \| \| \| \| \| \| \|	available from OCaml 3.11.2 (see bug #2707) - fixing outdated address for Coq Club git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14987 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correct application of head reduction.	msozeau	2012-02-20
\| \| \| \| \| \| \| \|	Fix a regression in subtac_pretyping, avoiding application of bidirectional application checking in case the return type is a subset (bad interaction with typeclass overloading). Should be done only on constructor applications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14985 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Document the [unify] tactic.	msozeau	2012-02-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14984 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix handling of space after "Notation" or "where", add missing keywords.	msozeau	2012-02-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14983 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Avoid retrying uncessarily to prove independent remaining obligations in ↵	msozeau	2012-02-15
\| \| \| \| \| \|	Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14982 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Avoid unnecessary normalizations w.r.t. evars in Program.	msozeau	2012-02-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14981 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and ↵	msozeau	2012-02-15
\| \| \| \| \| \|	us are not convertible git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14980 85f007b7-540e-0410-9357-904b9bb8a0f7
*	In [reflexivity], [symmetry] etc, use the type found by looking at the ↵	msozeau	2012-02-14
\| \| \| \| \| \| \| \|	relation as the carrier instead of the first argument's type (plays nicer with coercions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14979 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Fix dependency computation in eterm to not consider filtered variables.	msozeau	2012-02-14
\| \| \| \| \| \|	- Fix handling of evar map in Program coercion code that could forget some new declarations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14978 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Arguments supports extra notation scopes	gareuselesinge	2012-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14977 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Additional comment on Focus Conditions.	aspiwack	2012-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14975 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation for Grab Existential Variables.	aspiwack	2012-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A "Grab Existential Variables" to transform the unresolved evars at the end ↵	aspiwack	2012-02-07
\| \| \| \| \| \|	of a proof into goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14973 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo in comments.	aspiwack	2012-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correcting inversion in list of generated tcc of Function	letouzey	2012-02-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14967 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More information returned by coqtop about its internal state. Hopefully ↵	ppedrot	2012-02-02
\| \| \| \| \| \|	we'll manage to get rid of the own stack of coqide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14965 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix unblocking code in dependent destruction due to zeta being used in ↵	msozeau	2012-02-01
\| \| \| \| \| \|	unfold now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14964 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Corrected a careless cut-and-paste in Gallina description which dated back ↵	ppedrot	2012-02-01
\| \| \| \| \| \|	to 2003. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14963 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Debugger vs tracer: Two different behaviors wrt printing: The debugger	herbelin	2012-02-01
\| \| \| \| \| \| \| \| \|	runs in separate process. It has no access to the global env and it should not request it. The tracer runs in the same process as Coq and has full access to the global env and to regular pretty-printing of global names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14958 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improved synchronisation of stdlib index page with current library state.	herbelin	2012-02-01
\| \| \| \| \| \| \| \| \| \|	- Made generation of index page fail if a file is missing in list or listed but unbound in existing theories - Added a file hidden-files to optionally list library files not to show in the index page (though it is currently empty) - Added directory Unicode (why not to have it after all?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert "Tentative to fix bug #2628 by not letting intuition break records. ↵	msozeau	2012-01-31
\| \| \| \| \| \| \| \| \|	Might be too much of a backwards-incompatible change" Indeed it is breaking too many scripts. This reverts commit 47e9afaaa4c08aca97d4f4b5a89cb40da76bd850. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14956 85f007b7-540e-0410-9357-904b9bb8a0f7
*	index-list.html.template: add missing files	pboutill	2012-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14955 85f007b7-540e-0410-9357-904b9bb8a0f7