coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Improve readability the "lenses" in Proofview, using interfaces.	Arnaud Spiwack	2014-10-22
*	Proofview: clean up code a little.	Arnaud Spiwack	2014-10-22
*	Proofview: move [list_goto] to the [CList] module.	Arnaud Spiwack	2014-10-22
*	Proofview: replace the functions iter_list and iter_list2 by generic monadic ...	Arnaud Spiwack	2014-10-22
*	Add a two-list monadic fold_left iterator.	Arnaud Spiwack	2014-10-22
*	Small optimisation in the monadic list combinators.	Arnaud Spiwack	2014-10-22
*	Factor module signatures.	Arnaud Spiwack	2014-10-22
*	Proofview: clean up commented out code.	Arnaud Spiwack	2014-10-22
*	Proofview: remove a redundant primitive.	Arnaud Spiwack	2014-10-22
*	Proofview: move more functions to the Unsafe module.	Arnaud Spiwack	2014-10-22
*	Proofview: split [V82] module into [Unsafe] and [V82].	Arnaud Spiwack	2014-10-22
*	Proofview.mli: no more reference to Goal.goal.	Arnaud Spiwack	2014-10-22
*	Proofview: factor init and dependent_init.	Arnaud Spiwack	2014-10-22
*	Remove unused functions for side effects.	Arnaud Spiwack	2014-10-22
*	Remove the deprecated open-constr based refine.	Arnaud Spiwack	2014-10-22
*	Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.	Arnaud Spiwack	2014-10-22
*	Remove duplicate code.	Arnaud Spiwack	2014-10-22
*	Removing dead code in Rewrite.	Pierre-Marie Pédrot	2014-10-21
*	Small invariants in Rewrite code.	Pierre-Marie Pédrot	2014-10-21
*	Lazily check that an argument is dependent when constructing evar clauses.	Pierre-Marie Pédrot	2014-10-21
*	Fixing decompose_app_rel in Rewrite.	Pierre-Marie Pédrot	2014-10-21
*	Using new clausenv in rewrite.	Pierre-Marie Pédrot	2014-10-21
*	Adding an evar version of the make_clenv function.	Pierre-Marie Pédrot	2014-10-21
*	Porting Hugo's fix 98f3abb83a to native compiler.	Maxime Dénès	2014-10-21
*	Adapting output tests to the removal of the new token warning and to	Hugo Herbelin	2014-10-21
*	More precise test for #3459.	Hugo Herbelin	2014-10-21
*	Dead code.	Hugo Herbelin	2014-10-21
*	Continuing experimental printing of the signature of open evars in	Hugo Herbelin	2014-10-21
*	Removing re-typecheking from "refine" in no-check mode of the new	Hugo Herbelin	2014-10-20
*	Fixing a (new) part of bug #2729.	Hugo Herbelin	2014-10-20
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
*	Fixing a bug in the presence of let-in in inductive arity.	Hugo Herbelin	2014-10-20
*	Revert "Fixing a loop in proof reconstruction for congruence (#2447)."	Hugo Herbelin	2014-10-17
*	Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...	Hugo Herbelin	2014-10-17
*	Now printing "now a keyword" only in verbose mode.	Hugo Herbelin	2014-10-17
*	When facing problem ?id = ?id' in resolution of return predicate,	Hugo Herbelin	2014-10-17
*	Experimental printing of the signature of open evars in Check.	Hugo Herbelin	2014-10-17
*	New experimental heuristic printing strategy for evar instances: We	Hugo Herbelin	2014-10-17
*	Re-displaying evar instances in debugger.	Hugo Herbelin	2014-10-17
*	Fixing a loop in proof reconstruction for congruence (#2447).	Hugo Herbelin	2014-10-17
*	Essai où assert_style n'est utilisé que si pas visuellement une équation;	Hugo Herbelin	2014-10-17
*	More fallout from elisp rename	Anders Kaseorg	2014-10-16
*	Relaxing again the test on types of replacements in tactic change	Hugo Herbelin	2014-10-16
*	In convert_concl/convert_hyp: nf_enter -> enter.	Hugo Herbelin	2014-10-16
*	Revert "Naming main goal "Main""	Hugo Herbelin	2014-10-16
*	Refactoring proofview: make the definition of the logic monad polymorphic.	Arnaud Spiwack	2014-10-16
*	Refresh to avoid algebraic universes on the right.	Matthieu Sozeau	2014-10-16
*	Fix test-suite scripts.	Matthieu Sozeau	2014-10-16
*	Bug fixed by Hugo.	Matthieu Sozeau	2014-10-16
*	Grab Existential Variables: restore the goal order from v8.4.	Arnaud Spiwack	2014-10-16