coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	STM: code restructured to reuse task queue for tactics	Enrico Tassi	2014-08-05
*	Goal: API to get the solution of a goal	Enrico Tassi	2014-08-05
*	make a few lines fit the screen	Enrico Tassi	2014-08-05
*	STM: Classify Let as non asynchronous (Closes: #3486)	Enrico Tassi	2014-08-05
*	Coqide: annoying popups with GTK errors only in debug mode	Enrico Tassi	2014-08-05
*	Ring: prevent an error message to show in case of success.	Arnaud Spiwack	2014-08-05
*	Documentation: a simple example for [numgoals].	Arnaud Spiwack	2014-08-05
*	Ltac's [idtac] is now interpreted outside of a goal if possible.	Arnaud Spiwack	2014-08-05
*	Ltac's idtac is now implemented using the new API.	Arnaud Spiwack	2014-08-05
*	Tacinterp: [interp_message] and associate now only require an environment rat...	Arnaud Spiwack	2014-08-05
*	Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].	Arnaud Spiwack	2014-08-05
*	Documentation of [uconstr]: typesetting.	Arnaud Spiwack	2014-08-05
*	Documentation: refine accept uconstr arguments.	Arnaud Spiwack	2014-08-05
*	Doc: uconstr now has a tactic notation entry.	Arnaud Spiwack	2014-08-05
*	Fix interpretation bug in [uconstr].	Arnaud Spiwack	2014-08-05
*	The [refine] tactic now accepts [uconstr].	Arnaud Spiwack	2014-08-05
*	Small refactoring: use [uconstr] instead of [constr] when relevant in grammar...	Arnaud Spiwack	2014-08-05
*	Properly declare uconstr as an argument for TACTIC EXTEND.	Arnaud Spiwack	2014-08-05
*	Fix [uconstr] name for argextend.	Arnaud Spiwack	2014-08-05
*	Better fix of e5c025	Pierre Boutillier	2014-08-05
*	One more optimization for guard checking of cofixpoints.	Maxime Dénès	2014-08-04
*	More optimization in guard checking.	Maxime Dénès	2014-08-04
*	Fix an exponential behavior in guard checker for cofixpoints.	Maxime Dénès	2014-08-04
*	Fixing semantics of Univ.Level.equal.	Pierre-Marie Pédrot	2014-08-04
*	STM: when looking up in the cache catch Expired exc	Carst Tankink	2014-08-04
*	STM: generate Feedback message for parsing errors	Enrico Tassi	2014-08-04
*	STM: use a real priority queue	Enrico Tassi	2014-08-04
*	STM: encapsulate Pp.message in Feedback.feedback	Carst Tankink	2014-08-04
*	STM: VtQuery holds the id of the state it refers to	Carst Tankink	2014-08-04
*	Some comments in the interface of Proofview_monad.	Arnaud Spiwack	2014-08-04
*	Cleaning the new implementation of the tactic monad continued.	Arnaud Spiwack	2014-08-04
*	Cleaning of the new implementation of the tactic monad.	Arnaud Spiwack	2014-08-04
*	Fix to make Coq compile, I think this should still be accepted.	Matthieu Sozeau	2014-08-03
*	Fix infer conv using the wrong universe conversion flexibility information	Matthieu Sozeau	2014-08-03
*	- Fix handling of opaque polymorphic definitions which were turned transparent.	Matthieu Sozeau	2014-08-03
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	- Fix has_undefined_evars not using its or_sorts argument anymore.	Matthieu Sozeau	2014-08-03
*	Chapter 4: Fixing ambiguity about whether the return predicate refers	Hugo Herbelin	2014-08-03
*	Fixing #3483 (graceful failing with notations to non-constructors in "match").	Hugo Herbelin	2014-08-03
*	Better struture for Ltac internalization environments in Constrintern.	Pierre-Marie Pédrot	2014-08-02
*	Faster uconstr.	Arnaud Spiwack	2014-08-01
*	CHANGES: [>…].	Arnaud Spiwack	2014-08-01
*	Document [> … ].	Arnaud Spiwack	2014-08-01
*	New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.	Arnaud Spiwack	2014-08-01
*	Fix English spelling -> American spelling in doc.	Arnaud Spiwack	2014-08-01
*	CHANGES: [numgoals] and [guard].	Arnaud Spiwack	2014-08-01
*	Document [numgoals] and [guard].	Arnaud Spiwack	2014-08-01
*	Add [guard] tactic.	Arnaud Spiwack	2014-08-01
*	Add [numgoal] to Ltac.	Arnaud Spiwack	2014-08-01
*	Add primtive [num_goal] to Proofview.	Arnaud Spiwack	2014-08-01