coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Pass around information on the use of template polymorphism for	Matthieu Sozeau	2014-11-23
\| \| \| \| \| \| \|	inductive types (i.e., ones declared with an explicit anonymous Type at the conclusion of their arity). With this change one can force inductives to live in higher universes even in the non-fully universe polymorphic case (e.g. bug #3821).
*	One more word about "simpl f": avoid "simpl f" to be printed "simpl f",	Hugo Herbelin	2014-11-23
\| \| \| \|	at least when f is an evaluable reference.
*	Add printer for transparent state for ocamldebug.	Hugo Herbelin	2014-11-23
\|
*	Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc about	Hugo Herbelin	2014-11-23
\| \| \| \| \|	when the arguments of a constructor can be moved at the place of the variable on which destruct or induction applies.
*	Fix #3824. de Bruijn error in normalization of fixpoints.	Maxime Dénès	2014-11-23
\| \| \| \| \| \|	This bug was affecting the VM and the native compiler, but only in the pretyper (not the kernel). Types of arguments of fixpoints were incorrectly normalized due to a missing lift.
*	Specific printer of Evar.Set.t for ocamldebug + more information in	Hugo Herbelin	2014-11-22
\| \| \| \|	a UserError to ease debugging.
*	Attempt to organize and document unification flags of setoid rewrite.	Hugo Herbelin	2014-11-22
\|
*	Removing superfluous newlines in setoid_rewrite error message.	Hugo Herbelin	2014-11-22
\|
*	In setoid_rewrite error messages:	Hugo Herbelin	2014-11-22
\| \| \| \| \| \|	- removed the encapsulation in a Tactic Failure (I don't see why setoid_rewrite should specifically raise a Fail - do I miss something?) - avoid having twice a "Unable to satisfy ... constraints" message.
*	Test for closed #2713 and #2876.	Hugo Herbelin	2014-11-22
\|
*	Further simplifying functional induction.	Hugo Herbelin	2014-11-22
\|
*	Simplifying code of functional induction.	Hugo Herbelin	2014-11-22
\|
*	Not using an (arbitrary) pivot anymore for re-introduction of	Hugo Herbelin	2014-11-22
\| \| \| \| \| \| \|	quantified hypothesis in functional induction. This has apparently no visible effect, probably because functional schemes do not have non-dependent hypothesis in their branches besides induction hypotheses which are anyway introduced at the top of the context.
*	New simplification of code for generalizing hypotheses in destruct.	Hugo Herbelin	2014-11-22
\|
*	Removing a hack which, according to the comment, should not be necessary	Hugo Herbelin	2014-11-22
\| \| \| \|	anymore since "destruct eq_dec" works like "destruct (eq_dec _ _)".
*	Add test-suite file for dependent rewriting example by Vadim Zaliva and	Matthieu Sozeau	2014-11-22
\| \| \| \|	Daniel Schepler.
*	Fix resolve_morphism to build well-scoped terms in case some arguments	Matthieu Sozeau	2014-11-22
\| \| \| \|	of the function are dependent.
*	Enforcing the non-normalization of evars in Tactics.get_next_hyp_position.	Pierre-Marie Pédrot	2014-11-22
\|
*	Writing intro_replacing in the new monad.	Pierre-Marie Pédrot	2014-11-22
\|
*	Removing useless flag of the historical move tactic.	Pierre-Marie Pédrot	2014-11-22
\|
*	Exporting a primitive allowing to run completely the tactic monad.	Pierre-Marie Pédrot	2014-11-22
\|
*	Adding test for bug #3326.	Pierre-Marie Pédrot	2014-11-21
\|
*	Adding test for bug #3424.	Pierre-Marie Pédrot	2014-11-21
\|
*	Cleaning up closed bugs in test-suite.	Pierre-Marie Pédrot	2014-11-21
\|
*	Writing Tactics.keep in the new monad.	Pierre-Marie Pédrot	2014-11-21
\|
*	Test for bug #3788.	Pierre-Marie Pédrot	2014-11-21
\|
*	Add test-suite file for bug #3804.	Matthieu Sozeau	2014-11-21
\|
*	Fix bug #3804.	Matthieu Sozeau	2014-11-21
\|
*	Avoid compilation warning.	Matthieu Sozeau	2014-11-21
\|
*	Adding test for bug #3684.	Pierre-Marie Pédrot	2014-11-20
\|
*	Fixing the previous commit. We had to normalize evars first.	Pierre-Marie Pédrot	2014-11-20
\|
*	Somehow fixing a side-effect bug in tactics-in-terms.	Pierre-Marie Pédrot	2014-11-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Before this patch, when tactics-in-terms were relying on the ugly environment- modifying primitives such as tclABSTRACT, the returned term was ill-typed because the resulting effects were just dropped. Now we modify the returned term on the fly, effectively getting rid of the effects it may depend on. Yet, this is not completely satisfactory, because the tactic may solve some goals at distance (I would have said by side-effect, but this is ambiguous here). If ever the resulting terms are depending on the side-effects of the tactic, then we are still unsound. This patch should handle most of the use-cases gracefully. To really solve this issue, we should rewrite the pretyper in the new monad, which is easier said than done.
*	Probably useless use of a global-environment reading function in Indrec.	Pierre-Marie Pédrot	2014-11-20
\|
*	Exporting the function handling side-effects only applied to terms.	Pierre-Marie Pédrot	2014-11-20
\|
*	Re-removing the Hiddentac module. For some reason it had been reintroduced	Pierre-Marie Pédrot	2014-11-20
\| \| \| \|	by commit bf0185694.
*	Global.env chasing in Inv.	Pierre-Marie Pédrot	2014-11-20
\|
*	Adding locations to tclZEROMSG.	Pierre-Marie Pédrot	2014-11-20
\|
*	Setting printing flags on the printing of mutual inductives.	Pierre-Marie Pédrot	2014-11-20
\|
*	Moving mutual inductive printing from Printer to Printmod.	Pierre-Marie Pédrot	2014-11-20
\|
*	Making map_union a standard function of the ML library.	Hugo Herbelin	2014-11-19
\|
*	Slightly improving error messages when mismatch with Proof using at Qed time.	Hugo Herbelin	2014-11-19
\|
*	Option -type-in-type continued (deactivate test for inferred sort of	Hugo Herbelin	2014-11-19
\| \| \| \| \|	inductive types + deactivate test for equality of sort + deactivate the check that the constraints Prop/Set <= Type are declared).
*	Continuing fixing nested but convertible occurrences in find_subterm	Hugo Herbelin	2014-11-19
\| \| \| \| \|	(see 2e3ae20fe1e): test was only relevant in the case of explicitly given occurrence numbers.
*	Print [uconstr] in genargs.	Arnaud Spiwack	2014-11-19
\|
*	Print [uconstr]-s in [idtac] messages.	Arnaud Spiwack	2014-11-19
\|
*	Proper printer for [uconstr] in [Pptactic].	Arnaud Spiwack	2014-11-19
\| \| \| \|	This particular instance is probably never called though.
*	Printing function for [uconstr].	Arnaud Spiwack	2014-11-19
\| \| \| \|	The core is a "detyping" function for [closed_glob_constr]. Which interpretes the variable names according to the Ltac context, and apply the standard detyping procedure to typed terms in the closure.
*	uconstr: fix bug in interpretation of Ltac-bound name in let-tuple and ↵	Arnaud Spiwack	2014-11-19
\| \| \| \| \| \| \| \|	pattern-matching. In the syntax [let (x1,…,xn) := b in e] the name [x1…xn] were not interpreted with respect to the Ltac context. Hence typeable term would raise type-errors. The same problem also existed in pattern-matching.
*	Glob-ops: a name-mapping operation for pattern-matching binders.	Arnaud Spiwack	2014-11-19
\|
*	Adding rich-printing facilities to Printmod.	Pierre-Marie Pédrot	2014-11-19
\|