coq - The formal proof system

Age	Commit message (Collapse)	Author
2014-07-30	Avoid introducing additional universes when doing pruning in evarsolve.	Matthieu Sozeau

2014-07-29	CHANGES: untyped terms in tactics	Arnaud Spiwack

2014-07-29	Document untyped terms in tactics.	Arnaud Spiwack

2014-07-29	Small refactoring in Ltac parsing rules.	Arnaud Spiwack

2014-07-29	Allow [uconstr:c] as argument of a tactic.	Arnaud Spiwack

2014-07-29	Untyped terms in tactic: add the possibility to use a typed term inside an ↵	Arnaud Spiwack
	untyped term.
2014-07-29	Untyped terms in tactic: function [type_term c] to give a typed version of [c].	Arnaud Spiwack

2014-07-29	Untyped term in tactics: add an grammar entry to construct them.	Arnaud Spiwack
	The syntax is uconstr:term.
2014-07-29	Add a type of untyped term to Ltac's value.	Arnaud Spiwack
	It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218. The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.
2014-07-29	Clean up obsolete comment.	Arnaud Spiwack

2014-07-29	Add test-suite file for bug 3454.	Matthieu Sozeau

2014-07-29	Rework code for refolding projections in whd_state/whd_simpl to allow Arguments	Matthieu Sozeau
	Specifications indicating that the record object must be a constructor. Fixes bug #3432.
2014-07-29	Fix eta-conversion code which was failing in nested cases. Fixes bug #3429.	Matthieu Sozeau

2014-07-29	Add test-suite file for bug #3453	Matthieu Sozeau

2014-07-29	Fix bug #3453, not recognizing primitive projections in Coercion declarations.	Matthieu Sozeau

2014-07-29	Fix treatment of notations containing applications of projections (fixes bug ↵	Matthieu Sozeau
	#3454).
2014-07-29	STM: print goals with no duplicates	Enrico Tassi

2014-07-29	Pp: only one default feedback id	Enrico Tassi

2014-07-29	Pp compiles after feedback	Enrico Tassi

2014-07-28	CPS-style tactic matching. We use the tactic monad as the target of the CPS.	Pierre-Marie Pédrot
	This allows for tail-rec calls, prevents unwanted capture of closures and results in an overall more efficient evaluation.
2014-07-28	Adding a tclBREAK primitive to the tactic monad.	Pierre-Marie Pédrot

2014-07-27	Code cleaning in Tacenv.	Pierre-Marie Pédrot

2014-07-27	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot
	potentially conflicting tactics names from different plugins.
2014-07-25	Removing dead code relative to or_metaid.	Pierre-Marie Pédrot

2014-07-25	CHANGES: cycle and swap.	Arnaud Spiwack

2014-07-25	Document swap tactic.	Arnaud Spiwack

2014-07-25	Document cycle tactic.	Arnaud Spiwack

2014-07-25	Add a tactic [swap i j] to swap the position of goals [i] and [j].	Arnaud Spiwack
	If [i] or [j] is negative goals are counted from the end.
2014-07-25	Adds a cycle tactic to reorder goals in a loop.	Arnaud Spiwack
	[cycle 1] puts the first goal last, [cycle -1] puts the last goal first, [cycle n] is like [do n cycle 1], [cycle -n] is like [do n cycle -1].
2014-07-25	A slightly more fine grained way to check whether a TACTIC EXTEND is global ↵	Arnaud Spiwack
	or local to goals. Checks if the arguments need anything from the goal by looking at their tags, if not, the tactic is global.
2014-07-25	CHANGES: yellow in Coqide.	Arnaud Spiwack

2014-07-25	CHANGE: add Derive.	Arnaud Spiwack

2014-07-25	CHANGE: document the features of the new tactic engine.	Arnaud Spiwack

2014-07-25	Update the documentation of Ltac's ";" and ";[…]" to reflect the new ↵	Arnaud Spiwack
	multi-goal semantics of tactics.
2014-07-25	Warns about inconsistency of generated name in evars and goals.	Arnaud Spiwack
	See bug #1041
2014-07-25	- Do module substitution inside mind_record.	Matthieu Sozeau
	- Distinguish between primitive and non-primitive records in the kernel declaration, so as to try eta-conversion on primitive records only.
2014-07-25	More documentation of universes.	Matthieu Sozeau

2014-07-25	Add emacs auto-save and crash-save files to the .gitignore.	Arnaud Spiwack

2014-07-25	Add *.crashcoqide files to the .gitignore.	Arnaud Spiwack
	They occasionally show up while testing. I think it cleaner to ignore them.
2014-07-25	Add lia.cache to the .gitignore	Arnaud Spiwack

2014-07-25	Small reorganisation in proof.ml.	Arnaud Spiwack

2014-07-25	Fail gracefully when focusing on non-existing goals with user commands.	Arnaud Spiwack
	Fixes bug #3457
2014-07-25	Fix handling of universes at the end of proofs, esp. for async proof processing.	Matthieu Sozeau
	Thanks to E. Tassi for the initial patch.
2014-07-24	Forgot to add a Universes.v.tex as a target.	Matthieu Sozeau

2014-07-24	Start documenting universe polymorphism.	Matthieu Sozeau

2014-07-24	Distinguish tactics t1;t2 and t1;[t2..].	Arnaud Spiwack
	They used to be the same (and had a single entry in the AST). But now that t2 can be a multi-goal tactic, t1;[t2..] has the semantics of executing t2 in each goal independently.
2014-07-24	A handful of useful primitives in Proofview.Refine.	Arnaud Spiwack

2014-07-24	Fix misleading pretty-printing of information for non-universe-polymorphic	Matthieu Sozeau
	definitions.
2014-07-24	Adding a tail-rec tclONCE.	Pierre-Marie Pédrot

2014-07-24	New implementation of the tactic monad.	Pierre-Marie Pédrot
	The new implementation is made of two layers: a iolist, which is essentially a stream without memoization, and above this a state monad. The previous design of the extracted monad kept three distinct but similar monad transformers: a stateT, a writerT and a readerT. We take advantage of this similarity to pack those three transformers into only one state monad. This makes the code cleaner and hopefully more efficient.