coq - The formal proof system

Age	Commit message (Expand)	Author
2014-10-07	Removing debugging information committed by mistake.	Hugo Herbelin
2014-10-06	Make tclEFFECTS also update the env in the proof monad	Enrico Tassi
2014-10-05	Check compatibility of types in change depending on whether it is a	Hugo Herbelin
2014-10-03	Fixing #3657 (check that both sides of a "change with" have the same	Hugo Herbelin
2014-09-30	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin
2014-09-27	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau
2014-09-27	Changed semantics of induction !id when a clause is given: don't	Hugo Herbelin
2014-09-27	Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.	Pierre-Marie Pédrot
2014-09-24	Rename eq_constr functions in Evd to not break backward compatibility	Matthieu Sozeau
2014-09-24	Make eq_pattern_test/eq_test work up to the equivalence of primitive	Matthieu Sozeau
2014-09-17	Be more conservative and keep the use of eq_constr in pretyping/ functions.	Matthieu Sozeau
2014-09-17	Fix bug #3593, making constr_eq and progress work up to	Matthieu Sozeau
2014-09-17	Fix bug #3633 properly, by delaying the interpetation of constrs in	Matthieu Sozeau
2014-09-15	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau
2014-09-12	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-09-12	Commit 682aa67cc80 about enforcing that apply does not create new	Hugo Herbelin
2014-09-11	Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility...	Hugo Herbelin
2014-09-11	Other bugs with "inversion as" (collision between user-provided names and gen...	Hugo Herbelin
2014-09-10	A step towards better differentiating when w_unify is used for subterm	Hugo Herbelin
2014-09-10	More small bugs in intros_replacing.	Hugo Herbelin
2014-09-10	Fixing inversion after having fixed intros_replacing	Hugo Herbelin
2014-09-08	Fix [induction] wrt inductive records and non-recursive variants.	Arnaud Spiwack
2014-09-07	Fixing a bug in intros_replacing which was causing inversion not	Hugo Herbelin
2014-09-06	Fixing clearbody : typecheck definitions in context.	Pierre-Marie Pédrot
2014-09-06	Renaming goal-entering functions.	Pierre-Marie Pédrot
2014-09-05	Removing the old implementation of clear_body.	Pierre-Marie Pédrot
2014-09-05	At last a working clearbody!	Pierre-Marie Pédrot
2014-09-04	Revert the two previous commits. I was testing in the wrong branch.	Pierre-Marie Pédrot
2014-09-04	Removing the old implementation of clear_body.	Pierre-Marie Pédrot
2014-09-04	Reimplementing the clearbody tactic.	Pierre-Marie Pédrot
2014-09-04	Proofview refiner is now type-safe by default.	Pierre-Marie Pédrot
2014-09-04	Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.	Pierre-Marie Pédrot
2014-09-03	Yes another remaining clearing bug with 'apply in'.	Hugo Herbelin
2014-09-02	Another fix than 19a7a5789c to avoid descend_in_conjunction to use	Hugo Herbelin
2014-08-29	Not using a "cut" in descend_in_conjunctions induced more success. We	Hugo Herbelin
2014-08-27	Removing spurious tclWITHHOLES.	Pierre-Marie Pédrot
2014-08-25	Fixing previous commit.	Pierre-Marie Pédrot
2014-08-25	Fixing a bug introduced in the extension of 'apply in' + simplifying code.	Hugo Herbelin
2014-08-23	Tactics.is_quantified_hypothesis does not reduce anymore to decide whether	Pierre-Marie Pédrot
2014-08-23	Tactics.unify in the new monad.	Pierre-Marie Pédrot
2014-08-21	Removing unused parts of the Goal.sensitive monad.	Pierre-Marie Pédrot
2014-08-18	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin
2014-08-18	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin
2014-08-18	Slight simplification of naming of tactics in equality.ml (hopefully).	Hugo Herbelin
2014-08-18	A reorganization of the "assert" tactics (hopefully uniform naming	Hugo Herbelin
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin
2014-08-18	Reorganization of tactics:	Hugo Herbelin
2014-08-16	Fixing too restrictive detection of resolution of evars in "apply in"	Hugo Herbelin
2014-08-14	Restore the error-handling behavior of [change], which was silently failing	Matthieu Sozeau