coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Goptions do not rely anymore on generic equality.	Pierre-Marie Pédrot	2014-03-03
*	Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)	Pierre Letouzey	2014-03-02
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Adding an equality function over glob_constr	Pierre-Marie Pédrot	2014-03-02
*	Fixing pervasive comparisons	Pierre-Marie Pédrot	2014-03-01
*	Fixing bad comparison in Detyping.	Pierre-Marie Pédrot	2014-03-01
*	Removing Pervasives.compare in Termdn.	Pierre-Marie Pédrot	2014-02-28
*	Removing a Pervasives.compare in Term_dnet.	Pierre-Marie Pédrot	2014-02-28
*	Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infini...	Pierre Boutillier	2014-02-28
*	Dead code elimionation in reductionops	Pierre Boutillier	2014-02-28
*	Tacinterp: refactoring using Monad.	Arnaud Spiwack	2014-02-27
*	Code refactoring thanks to the new Monad module.	Arnaud Spiwack	2014-02-27
*	remoteCounter: backup/restore	Enrico Tassi	2014-02-26
*	IStream: change type of thunk, spare allocations.	Arnaud Spiwack	2014-02-24
*	Ensuring that the module Stack is opaque inside Reductionops.	Pierre-Marie Pédrot	2014-02-24
*	cbn understands Arguments	Pierre Boutillier	2014-02-24
*	Simpl_behaviour becomes Reductionops.ReductionBehaviour	Pierre Boutillier	2014-02-24
*	Create Debug Unification option	Pierre Boutillier	2014-02-24
*	No more translation array <-> list in Reductionops.Stack	Pierre Boutillier	2014-02-24
*	Reductionops.Stack.strip* are ready to deal with Shift	Pierre Boutillier	2014-02-24
*	Reductionops.Stack.app_node is secret	Pierre Boutillier	2014-02-24
*	app_node, stack, state printers	Pierre Boutillier	2014-02-24
*	Stack operations of Reductionops in Reductionops.Stack	Pierre Boutillier	2014-02-24
*	TC: honor the use_typeclasses flag in pretyping	Enrico Tassi	2014-02-12
*	Made Pre_env.lazy_val opaque.	Pierre-Marie Pédrot	2014-02-11
*	Tracking memory misallocation by trying to improve sharing.	Pierre-Marie Pédrot	2014-02-03
*	Using Map.smartmap whenever deemed useful.	Pierre-Marie Pédrot	2014-01-29
*	Abstracting away coercion indexes in Classops.	Pierre-Marie Pédrot	2014-01-27
*	Coercions: avoid imperative data structure	Enrico Tassi	2014-01-26
*	STM: additional fix for STM + vm_compute	Enrico Tassi	2014-01-07
*	When resetting an evarmap with the unsafe function Evd.evars_reset_evd with	Pierre-Marie Pédrot	2013-12-30
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Fix test-suite/success/evars.v.	Arnaud Spiwack	2013-12-06
*	Removing useless meta-related functions.	Pierre-Marie Pédrot	2013-12-03
*	Better heuristic for name generation backward compatibility. We fallback	Pierre-Marie Pédrot	2013-11-30
*	Useless instantiation function exported in Evd.	Pierre-Marie Pédrot	2013-11-30
*	Tentative fix to recover fresh name generation as it was before	Pierre-Marie Pédrot	2013-11-30
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Factoring: is_section_variable.	Arnaud Spiwack	2013-11-25
*	Typo resulting in bad eta-expansion of destructing let's body.	Hugo Herbelin	2013-11-25
*	Update comments in matching.mli.	aspiwack	2013-11-14
*	Removing partial applications in Reductionops.	ppedrot	2013-11-08
*	Partial application hunt.	ppedrot	2013-11-07
*	Less partial applications in Vars, as well as better memory allocation.	ppedrot	2013-11-06
*	Preventing useless allocations in Reductionops.instance.	ppedrot	2013-11-05
*	Nicer infered names in refine.	aspiwack	2013-11-04
*	push_rel_context: do not rename section variables.	aspiwack	2013-11-02
*	Fix compilation of pattern matching wrt variables: alias.	aspiwack	2013-11-02