coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Activating flags betaiota by default for apply	herbelin	2011-06-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14220 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r14204 and 14218 continued: completely removing test for bug #2490,	herbelin	2011-06-18
\| \| \| \| \| \| \|	leaving the decision of what to do with it to Matthieu; sorry for the confusion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14219 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Partial backtrack on wrong r14204: bug #2490 still open.	herbelin	2011-06-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14218 85f007b7-540e-0410-9357-904b9bb8a0f7
*	The ad hoc version for first-order unification at toplevel of "?n args	herbelin	2011-06-18
\| \| \| \| \| \| \| \| \| \| \|	= t" introduced in r14199 (w_typed_unify_list) tried to check types of metas more than what w_typed_unify used to before (and these types need delta to be convertible). Don't know if it is a weakness of the test for checking types but since checking types should not be necessary here, w_typed_unify_list now follows what w_unify_core_0 does more closely. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14217 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo in CHANGES	herbelin	2011-06-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14216 85f007b7-540e-0410-9357-904b9bb8a0f7
*	add names of theorems in output	jnarboux	2011-06-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14215 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Customized accelerator maps for macos are globally installed (end to fix 2462)	pboutill	2011-06-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14214 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix 2516: Utf8 font in Coqide Command panel	pboutill	2011-06-17
\| \| \| \| \| \|	Not perfect, font of unactives command panels won't change on the fly. (As it is for others GtextArea.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14213 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug 2269, program typechecker not used in Instance conclusions	msozeau	2011-06-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14212 85f007b7-540e-0410-9357-904b9bb8a0f7
*	refman nsatz	pottier	2011-06-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14211 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tests de nsatz avec la geometrie	pottier	2011-06-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14210 85f007b7-540e-0410-9357-904b9bb8a0f7
*	git rebase -i mess consequence	pboutill	2011-06-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14209 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert "Coqide now need lablgtk2.14.0" + Ide build system debugging	pboutill	2011-06-14
\| \| \| \| \| \| \| \|	We can be easily substitute Gdk.Windowing by a glance of configure work... This reverts commit 8b6f6b1c4b60e74dccd5d8c49bdd433e19d53bf4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14208 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Making printing of backtick in Program reparsable (avoiding collision with "`(")	herbelin	2011-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14205 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Regression files for bugs #2304 and #2490.	herbelin	2011-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14204 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bug #2181 (Class mechanism can create dependencies over unnamed	herbelin	2011-06-14
\| \| \| \| \| \|	fields of records). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14201 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A few comments and a dev file to summarize issues with unification	herbelin	2011-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14200 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added full pattern-unification on Meta for tactic unification.	herbelin	2011-06-13
\| \| \| \| \| \| \|	No way to control it yet; maybe flag use_evars_pattern_unification should be generalized for that purpose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14199 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a flag to restrict conversion in tactic unification on the	herbelin	2011-06-13
\| \| \| \| \| \| \| \| \|	strict subterms of the initial unification problem (inspired from ssreflect rewriting strategy). Not activated however (a few applications of setoid rewrite use this possibility on closed terms in the stdlib, e.g. "flip le p (min n m)" identified with "le (min n m) p"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14198 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Another bug of Scheme Induction (generated names dep/nodep were swapped).	herbelin	2011-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14195 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing an anomaly in Scheme Induction.	herbelin	2011-06-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14193 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oups, typo in previous commit	herbelin	2011-06-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14192 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removed what looks like a (very old) useless f.o. unification pass	herbelin	2011-06-12
\| \| \| \| \| \|	made after s.o. unification succeeds. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14191 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	flag to forbid rewriting tactics to instantiate an evar of the goal while looking for subterms (this is not clear that we always want that for rewrite but we certainly want it for autorewrite; see comments by Charguéraud on coqdev Oct 2010). In a few cases in the theories, a pre-existing evar of an hyp used for rewriting is instantiated by the rewriting step. Let's accept this at the current time. We have to make progress towards documenting and stabilizing the strategy for matching/unifying subterms in rewrite/induction/set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14190 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rather quick hack to avoid using notations involving "Type" when	herbelin	2011-06-12
\| \| \| \| \| \| \|	Universes Printing is on. Code of Topconstr.match_ becomes a bit cluttered, used abbreviation to shorten it (just) a little. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14189 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide now need lablgtk2.14.0	pboutill	2011-06-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14188 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated CHANGES (info, Show Script, rephrasing).	herbelin	2011-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14187 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moved allow_K to a unification flag	herbelin	2011-06-10
\| \| \| \| \| \| \| \|	- seized the opportunity to align unification flags for functional induction to the ones of induction - also tried to add delta in the elim_flags used in tactics.ml - also tried to unify the rewrite flags in concl or in hyp (removed allow_K in hyps) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14186 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing another bug with "_" intro pattern.	herbelin	2011-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14185 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing the "buggy" first_name and prepare multi-induction.	herbelin	2011-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14184 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Made use of "_" in repeated use of intros_patterns work (with	herbelin	2011-06-10
\| \| \| \| \| \|	application to "destruct t as (_,H)" in the dependent case, and so on). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14183 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Integrating onLastHypId into intro so that we can get the introduction	herbelin	2011-06-10
\| \| \| \| \| \| \|	name even when the hyp has not been introduced at the top of the context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14182 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Call process_vernac_interp_error before calling Errors.print in	herbelin	2011-06-10
\| \| \| \| \| \| \| \|	plugins so that errors are indeed processed. Not sure this is the best way to do it. Maybe funind should use with_heavy_rollback for delimitating its use of vernac commands. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14181 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide Menubar integration in MacOS	pboutill	2011-06-10
\| \| \| \| \| \|	Because of lablgtk issues, accel_maps can't be customized well on MacOS git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14180 85f007b7-540e-0410-9357-904b9bb8a0f7
*	no more errors at _stubs.c.d generation	pboutill	2011-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14179 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Menubar and toolbar in coqide using GtkUI & Gactions.	pboutill	2011-06-10
\| \| \| \| \| \| \| \| \|	You'll need to remove/edit your ~/.coqiderc and ~/.coqide.keys. As it used to be, accelerator modifiers changes are only done after a reboot but we need more binding in lablgtk to improve that... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14178 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert "Check if recursive calls are guarded before printing "Proof completed"."	pboutill	2011-06-10
\| \| \| \| \| \| \| \| \| \| \|	because guard condition is checked at Qed anyway and it can be expensivise to check it twice. Use explicitly "Guarded" if you want this information. But the wrong proof completed is now the right no more subgoals ... Of course, we would like an incrementally checked guard condition one day ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14177 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixes in pruning, do not fail if pruning is impossible due to typing ↵	msozeau	2011-06-10
\| \| \| \| \| \|	constraints but postpone evar-evar problems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14176 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ring2, cring, nsatz avec type classe avec parametres plus notations	pottier	2011-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14175 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More fixes in pruning/restriction of evars during unification.	msozeau	2011-06-09
\| \| \| \| \| \| \| \|	- Do not allow to filter variables that appear in the conclusion of an evar. - Do not attempt to restrict evars based on a substitution that does not contain only evars (fall back to the pattern fragment and do not lose solutions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14174 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Make Notation works with anonymous-level "Type".	herbelin	2011-06-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14170 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixes in pruning in unification.	msozeau	2011-06-08
\| \| \| \| \| \| \| \| \|	Properly normalize evars to reflect the already pruned evars in the type of dependent evars to allow more precise restriction of hyps. Directly check the type of an evar instance, allowing backtracking on ill-typed instanciations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14169 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #2399 in Program: used to build an ill-formed term due to a de ↵	msozeau	2011-06-07
\| \| \| \| \| \|	Bruijn bug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14168 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity ↵	msozeau	2011-06-07
\| \| \| \| \| \|	proofs create unsolved evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14167 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Catch AbstractionOverMeta as a unification failure in precatchable_exception.	msozeau	2011-06-07
\| \| \| \| \| \|	Allows rewrite H in * \|- to work in case a rewrite throws this exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14166 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug #2415: warn when closing modules or sections and some obligations ↵	msozeau	2011-06-07
\| \| \| \| \| \|	are unresolved git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14165 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.	msozeau	2011-06-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14164 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Fix restrict_hyps to not allow filtering on a variable required to ↵	msozeau	2011-06-07
\| \| \| \| \| \| \| \| \|	typecheck the evar's conclusion - Prevent extend_evar from creating ill-formed evars with de Bruijn-open conclusions. - Minor fix of define_evars_as_lambda, another mixup of named and de Bruijn indices. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14163 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo.	gmelquio	2011-06-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14162 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mini-test for eta	herbelin	2011-05-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14160 85f007b7-540e-0410-9357-904b9bb8a0f7