coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing pervasive comparisons	Pierre-Marie Pédrot	2014-03-01
*	Removing a fishy use of pervasive equality in Ltac backtrace printing.	Pierre-Marie Pédrot	2014-03-01
*	Removing Pervasives.compare in Termdn.	Pierre-Marie Pédrot	2014-02-28
*	Tacinterp: more refactoring.	Arnaud Spiwack	2014-02-27
*	Tacinterp: refactoring using Monad.	Arnaud Spiwack	2014-02-27
*	Code refactoring thanks to the new Monad module.	Arnaud Spiwack	2014-02-27
*	Remove unsafe code (Obj.magic) in Tacinterp.	Arnaud Spiwack	2014-02-27
*	Proofview.Notations: Now that (>>=) is free, use it for tclBIND.	Arnaud Spiwack	2014-02-27
*	Get rid of the enterl/glist API for Proofview.Goal.	Arnaud Spiwack	2014-02-27
*	Tacinterp: yet another superfluous enterl.	Arnaud Spiwack	2014-02-27
*	Tacinterp: spurious enterl.	Arnaud Spiwack	2014-02-27
*	Dead code: eval_ltac_constr.	Arnaud Spiwack	2014-02-27
*	Tacinterp: remove the is_value check in Ltac's let-in.	Arnaud Spiwack	2014-02-25
*	Tacinterp: fewer enterl still.	Arnaud Spiwack	2014-02-25
*	Tacinterp: fewer Proofview.Goal.enterl.	Arnaud Spiwack	2014-02-25
*	Tacinterp: clean up.	Arnaud Spiwack	2014-02-25
*	Tacinterp: remove unnecessary return/bind pairs.	Arnaud Spiwack	2014-02-25
*	TacticMatching: avoid some closure allocation in (<*>).	Arnaud Spiwack	2014-02-24
*	Removed some trailing whitespaces.	Arnaud Spiwack	2014-02-24
*	IStream: a concat_map primitive.	Arnaud Spiwack	2014-02-24
*	A view type for IStream.	Arnaud Spiwack	2014-02-24
*	Removing non-marshallable data from the Agram constructor. Instead of	Pierre-Marie Pédrot	2014-02-16
*	The constructor tactic now returns several successes.	Pierre-Marie Pédrot	2014-02-04
*	Fixing bug #3226.	Pierre-Marie Pédrot	2014-02-02
*	In Ltac's exact tactic: avoid checking the type of the term twice.	Arnaud Spiwack	2014-01-31
*	Fixing dependent inversion. Some exceptions were not caught by the tactic	Pierre-Marie Pédrot	2014-01-28
*	Adding a default object to generic argument registering mechanism.	Pierre-Marie Pédrot	2014-01-19
*	Fixing bug #1758: Print Hint output can be misleading if variable shadows hyp...	Pierre-Marie Pédrot	2014-01-17
*	Removing unused tactics in rewrite.	Pierre-Marie Pédrot	2014-01-14
*	Exporting the full pretyper options in Goal.constr_of_raw.	Pierre-Marie Pédrot	2014-01-10
*	Fix bug#2080: error message on Ltac name clash with primitive tactics	xclerc	2014-01-10
*	Algebraized "No such hypothesis" errors	Pierre-Marie Pédrot	2014-01-06
*	Code cleaning in Rewrite, may also result faster.	Pierre-Marie Pédrot	2014-01-04
*	Qed: feedback when type checking is done	Enrico Tassi	2013-12-24
*	Simplifying the use of hypinfos in Rewrite.	Pierre-Marie Pédrot	2013-12-24
*	Rewrite.ml: removing direction flag from hypinfo.	Pierre-Marie Pédrot	2013-12-23
*	Do not pass unification flags around in Rewrite.	Pierre-Marie Pédrot	2013-12-22
*	Slight code cleaning ensuring more static invariants in Rewrite.	Pierre-Marie Pédrot	2013-12-22
*	Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at	Pierre-Marie Pédrot	2013-12-22
*	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot	2013-12-19
*	Using interp_genarg in tactic notations where possible, instead of an ad-hoc	Pierre-Marie Pédrot	2013-12-19
*	Bad use of Obj.magic in interpretation of TacAlias arguments.	Pierre Boutillier	2013-12-19
*	Printing function for Stdargs in debugger	Pierre Boutillier	2013-12-19
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
*	Get rid of messages "emitting ..." when compiling .v files	Pierre Letouzey	2013-12-16
*	Dedicated inductive for return values of rewrite strategies.	Pierre-Marie Pédrot	2013-12-16
*	Fixing backtrace registering of various tactic-related try-with blocks.	Pierre-Marie Pédrot	2013-12-11
*	Stylistic change.	Arnaud Spiwack	2013-12-09
*	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack	2013-12-04
*	Porting type interpretation in Tacinterp to the new tactics.	Pierre-Marie Pédrot	2013-12-02