coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	nat_iter n f x -> nat_rect _ x (fun _ => f) n	pboutill	2012-12-21
*	Yet a new reduction tactic in Coq : cbn	pboutill	2012-12-21
*	Awful heuristic to refold mutual fixpoint in reductionops	pboutill	2012-12-21
*	Fixup and comment reductionops	pboutill	2012-12-21
*	Reductionops reduction machine can refold constant	pboutill	2012-12-19
*	Evarconv.Pseudorigid erasure	pboutill	2012-12-19
*	Coqide: cleaner Coq.PrintOpt and session creation	letouzey	2012-12-19
*	Array.create is deprecated	pboutill	2012-12-19
*	GtkData.set_default_modifiers and no access to <primary> in lablgtk -> unsuab...	pboutill	2012-12-19
*	Fix coqtop -config when absolute path have been given for ocaml*	pboutill	2012-12-19
*	Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)	letouzey	2012-12-18
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of mod_bound_id	ppedrot	2012-12-18
*	Modulification of Label	ppedrot	2012-12-18
*	Fixing parsing of specific primitive tokens used as notations for patterns	herbelin	2012-12-18
*	Taking into account the possibility of having a type of type which is	herbelin	2012-12-18
*	Extraction: qualified names in Extract Constant examples (fix #2878)	letouzey	2012-12-18
*	No more constant named "int" in Coq theories (cf bug #2878)	letouzey	2012-12-18
*	Fixed a little inefficiency of "set/destruct" over a pattern. Now	herbelin	2012-12-18
*	Factorization of the elim unif flag with the default flag. Since	herbelin	2012-12-18
*	Fixed interpretation of "x" as a binding variable for the return	herbelin	2012-12-17
*	Do not display REVERTcast inserted by reduction tactics (unless printing all).	herbelin	2012-12-17
*	Fixed a bug in the algorithm trying to elaborate a "match" return predicate.	herbelin	2012-12-17
*	Ide_slave: do not prepare debug messages in non-debug mode	letouzey	2012-12-17
*	Extraction of projections: restrict a hack to ocaml only (fix #2941)	letouzey	2012-12-17
*	Fixing ocalmdoc comment	ppedrot	2012-12-14
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Fixing CoqIDE compilation	ppedrot	2012-12-14
*	Moving hcons_string to String namespace.	ppedrot	2012-12-14
*	Moved Stringset and Stringmap to String namespace.	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Implemented a full-fledged equality on [constr_expr]. By the way,	ppedrot	2012-12-14
*	Using library string functions.	ppedrot	2012-12-13
*	Documented CString.	ppedrot	2012-12-13
*	Renamed Option.Misc.compare to the more uniform Option.equal.	ppedrot	2012-12-13
*	Wg_ScriptView: avoid invalid iters during completion	letouzey	2012-12-11
*	Coqide: allow editing even during a backtrack	letouzey	2012-12-11
*	Coq_lex: direct accounting of utf8 extra bytes in offsets	letouzey	2012-12-11
*	Coqide: restore the tag removal of copy-pasted zones	letouzey	2012-12-10
*	Coqide: some more refactoring to lighten coqide.ml	letouzey	2012-12-10
*	Coq_makefile: Better rule for subdirs when the subdir does not exist	pboutill	2012-12-10
*	Tiny fix of r16049	pboutill	2012-12-10
*	* Implementing the "union by rank" optimisation in univ.ml	pboutill	2012-12-10
*	Ensure that a function declared with a label is used with it	letouzey	2012-12-08
*	Finish patch for Hint Resolve, stopping to generate new constant names for	msozeau	2012-12-08
*	Coqide: use labels for all labelled functions	letouzey	2012-12-08
*	Coqide: handle possible fragmentation in xml answers	letouzey	2012-12-08
*	Coqide: get rid of threads, use gtk asynchronous i/o instead	letouzey	2012-12-08
*	Removed a unused function in Pp	ppedrot	2012-12-08