coq - The formal proof system

Age	Commit message (Expand)	Author
2013-11-04	Allowing proofs starting with a non-empty evarmap.	ppedrot
2013-11-04	Using allocation-free version of Array higher-order function in critical	ppedrot
2013-11-04	Adding closure-preventing functions in CArray. These functions are all	ppedrot
2013-11-04	Allocation friendly version of Util.iterate.	ppedrot
2013-11-04	Added an update function in CMap. It has the same signature as Map.add, but	ppedrot
2013-11-04	Manual coding of Int.Map.find. We use unsafe features, but this function	ppedrot
2013-11-04	Evar module now uses default Int maps and sets.	ppedrot
2013-11-03	empty token in terminal is a user error not an anomaly (bug 3118)	pboutill
2013-11-03	test-suite fixup	pboutill
2013-11-03	Asks camlp5 binary in path its location	pboutill
2013-11-03	Fixup bug 3145	pboutill
2013-11-03	configure stript allows make v4.00	pboutill
2013-11-02	Fixing CAMLP4 compilation.	ppedrot
2013-11-02	Fix set: nf_evar prior to tactic interpretation.	aspiwack
2013-11-02	Plug back infoH.	aspiwack
2013-11-02	Plugs back external tactics.	aspiwack
2013-11-02	Fix the log of debug auto.	aspiwack
2013-11-02	A try/with was catching every exception.	aspiwack
2013-11-02	Update comments.	aspiwack
2013-11-02	Doc: solve the bad interaction between Declare Implicit Tactic and refine.	aspiwack
2013-11-02	Cleanup of comments in bootstrap/Monads.v	aspiwack
2013-11-02	The repeat tactic now honors failure levels in ltac.	aspiwack
2013-11-02	Documentation for the backtracking features.	aspiwack
2013-11-02	Fix destruct: nf_evar prior to tactic interpretation.	aspiwack
2013-11-02	Tacticals.New.tclWITHHOLES: clean up.	aspiwack
2013-11-02	Fix congruence: normalise hypotheses with respect to evars.	aspiwack
2013-11-02	Add primitives in Goal.V82 to access the goal in nf_evar'd form.	aspiwack
2013-11-02	push_rel_context: do not rename section variables.	aspiwack
2013-11-02	Refine now does iota reduction in addition to beta.	aspiwack
2013-11-02	Fix compilation of pattern matching wrt variables: alias.	aspiwack
2013-11-02	Restore Zsqrt compat now that refine works fine with match.	aspiwack
2013-11-02	Fix the compilation of pattern matching wrt to variables.	aspiwack
2013-11-02	Refine: Tactics.New.refine does beta-reduction.	aspiwack
2013-11-02	Adds a tactic give_up.	aspiwack
2013-11-02	A tactic shelve_unifiable.	aspiwack
2013-11-02	Made multiple-goal tactic work after all: .	aspiwack
2013-11-02	Make multiple-goal tactics possible after a tclTHEN.	aspiwack
2013-11-02	Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used ...	aspiwack
2013-11-02	Adds a shelve tactic.	aspiwack
2013-11-02	bootstrap/Monad.v: implements the writer monad in continuation passing style.	aspiwack
2013-11-02	bootstrap/Monad.v: implements the environment monad in continuation passing s...	aspiwack
2013-11-02	Factors the lifting of environment and writer monads in bootstrap/Monad.v	aspiwack
2013-11-02	Adds an experimental exactly_once tactical.	aspiwack
2013-11-02	Normalise goals with respect to evars in the new tactics.	aspiwack
2013-11-02	Made Proofview.Goal.hyps a named_context.	aspiwack
2013-11-02	Refine does beta-reductions.	aspiwack
2013-11-02	A dedicated view type for Proofview_gen.split.	aspiwack
2013-11-02	Adds a tactical once.	aspiwack
2013-11-02	Corrects the semantics of the "+" tactical.	aspiwack
2013-11-02	Less use of the list-based interface for goal-bound tactics.	aspiwack