coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Improving pretty-printing of Ltac functions.	herbelin	2011-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14801 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing format of complexity bug Notations.v.	herbelin	2011-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14800 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing previous commit which was bugging on tactics preceded by goal number ↵	courtieu	2011-12-16
\| \| \| \| \| \|	(2:intros.). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14799 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide: adapt some comments now that bullets are terminators like { }	letouzey	2011-12-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14798 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
\| \| \| \| \| \| \| \| \| \| \| \|	known in advance to be instantiable by only a finite number of terms. When an evar with candidates remain unsolved after unification, the first candidate is taken as a heuristic. This is used in particular to reduce the number of pending conversion problems when trying to infer the return clause of a pattern-matching problem. As an example, this repairs test 2615.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14797 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin	2011-12-16
\| \| \| \| \| \| \| \|	printing notations. Since notation printing is not typed, printing "F G" using a notation for "f (fun x => g)" recursively eta-expands G, then x, then a new x and so on forever. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14796 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adapting coqide to my last commit:	courtieu	2011-12-16
\| \| \| \| \| \| \| \|	Moving bullets (-, +, *) into stand-alone commands instead of being part of a tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14795 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moving bullets (-, +, *) into stand-alone commands instead of being	courtieu	2011-12-16
\| \| \| \| \| \| \| \|	part of a tactic. WARNING: Coqide needs to be adapted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14794 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaned up a bit goal handling in Coqtop interface. Now we have two queries ↵	ppedrot	2011-12-15
\| \| \| \| \| \|	: goal description, with focused and unfocused goals, and list of currently declared evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14793 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Some extra universe refreshing seems needed in abstract_generalize	herbelin	2011-12-14
\| \| \| \| \| \|	(for generalize_eqs). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14792 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CHANGES: some more updates	letouzey	2011-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14791 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Proof using ...	gareuselesinge	2011-12-12
\| \| \| \| \| \| \| \| \| \| \| \| \|	New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction: only do the test on generalizable lets for ocaml	letouzey	2011-12-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14785 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: force the installation of all .cmi (and remove some obsolete .mli)	letouzey	2011-12-08
\| \| \| \| \| \| \|	The previous code wasn't detecting and installing .cmi coming from .mli without corresponding .ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14783 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction: avoid internal eta-reduction (fix #2570)	letouzey	2011-12-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14782 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing grammar resetting bug in the presence of levels initially empty	herbelin	2011-12-07
\| \| \| \| \| \|	(the number of entries to reset was not correct). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14778 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adapting test Existentials to new numbering strategy of evars (r14764).	herbelin	2011-12-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14777 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing a bug of commit r13310 (activating coercions only when module	herbelin	2011-12-07
\| \| \| \| \| \| \|	is imported): in case of nested modules, activation was done as soon as the outermost module was imported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14775 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Html page titles	pboutill	2011-12-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14774 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Vectors use a bit more the pattern matching compiler	pboutill	2011-12-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14773 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	pboutill	2011-12-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14772 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a synchronization bug between coqtop and the CoqIDE command pane.	ppedrot	2011-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14771 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fix Makefile.common handling of -byte-only	gareuselesinge	2011-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14770 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of Arguments + implicits	gareuselesinge	2011-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14769 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation for Arguments + notation scopes	gareuselesinge	2011-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14768 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation for Arguments + simpl	gareuselesinge	2011-12-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14767 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor fixes to Arguments	gareuselesinge	2011-12-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Implicit arguments can be mentioned anonymously: Arguments map {_ _} f l. - To rename implicit arguments, the ": rename" flag must be used: Arguments map {T1 T2} f l : rename. Without the ": rename" flag arguments can be used to assert that a function has indeed the expected number of arguments and that the arguments are named as expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14766 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack on synchronizing universe counter with reset	herbelin	2011-12-06
\| \| \| \| \| \|	mechanism, section discharge is not ready for that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14765 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Registering universe and meta/evar counters as summaries so as to	herbelin	2011-12-05
\| \| \| \| \| \| \| \|	eventually get the same numbers when replaying (but does not work for Undo/Abort which are still not plugged to the summary freezing mechanism). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14764 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Yet another fix about alias in testing if pattern unification applies.	herbelin	2011-12-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14763 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bugs in doc about when "with" is needed or not to give bindings	herbelin	2011-12-04
\| \| \| \| \| \|	to tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a small regression in pattern-matching compilation introduced in	herbelin	2011-12-04
\| \| \| \| \| \| \| \| \|	r14737 (when to expand an alias). However, the heuristic remains different as before r14737 since we stopped taking into account the dependency in the predicate to take the decision of expanding or not. Let's see if we can eventually fine-tuning this. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14760 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A small test for type inference (used to be a regression at some time).	herbelin	2011-12-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14759 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing superflous newline in output of About when no parameter is renamed.	herbelin	2011-12-04
\| \| \| \| \| \| \| \| \|	Fixing output tests after having added flushing of warning in revisions 14747 and 14750. Moving Implicit output test to new command Arguments. Adding test of new Arguments syntax in PrintInfos.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Discarding let-ins from the instances of the evars in the	herbelin	2011-12-04
\| \| \| \| \| \| \| \| \| \|	pattern-unification test. They were tolerated up to r14539. Also expanded the let-ins not bound to rel or var in the right-hand side of a term for which pattern-unification is tested (this expansion can refer to a non-let variable that has to be taken into account in the pattern-unification test). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14757 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a bug introduced in r12755. CoqIDE would ignore the Printing ↵	ppedrot	2011-11-30
\| \| \| \| \| \|	Existential Instances options because it was ill-formed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14756 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction: try to avoid issues with an Include directly inside a .v	letouzey	2011-11-30
\| \| \| \| \| \| \| \| \| \|	This concerns only "monolithic" extraction (and not Extraction Library). Typical situation is Vector.v containing an Include VectorDef. Cf. the test-case of bug #2570. Also kills two lines of dead code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14755 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Now CoqIDE relies on the option query mechanism to set printing options. ↵	ppedrot	2011-11-30
\| \| \| \| \| \|	Still a bit hackish. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14754 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More type safety in query GADT (again).	ppedrot	2011-11-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14753 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a serious bug in XML marshalling due to unsafe GADTs. Now types are ↵	ppedrot	2011-11-30
\| \| \| \| \| \|	enforced through hand-made casts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14751 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Continuing r14747 being actually incomplete (flushing warnings and	herbelin	2011-11-30
\| \| \| \| \| \|	printing them only if verbose). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14750 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Quick hack to avoid anomaly on using Program w/o having required JMeq.	herbelin	2011-11-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14749 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Preventing Implicit Arguments warning to be shown in non verbose mode	herbelin	2011-11-30
\| \| \| \| \| \|	+ flushing printing of the message . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14747 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation of appcontext	letouzey	2011-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14744 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed a warning about unused variable introduced in r14731	ppedrot	2011-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14743 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lib/xml_lexer.ml in .gitignore (produced by a .mll)	letouzey	2011-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14742 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extraction: typo in last commit	letouzey	2011-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14741 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fix for bug #2649	corbinea	2011-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14740 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Term: properly ignore Casts between Apps in constr_ord	puech	2011-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14739 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Term: useless conversion to list in constr_ord deleted	puech	2011-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14738 85f007b7-540e-0410-9357-904b9bb8a0f7