aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-01-07Coq_makefile: quoting pathspboutill
2013-01-07Coq_makefile: -extra & -phony-extra for user defined makefile rulepboutill
2013-01-07Fixup notation printing in patternspboutill
2013-01-06* Kernel/Terms:regisgia
2012-12-22Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located.herbelin
2012-12-21nat_iter n f x -> nat_rect _ x (fun _ => f) npboutill
2012-12-21Yet a new reduction tactic in Coq : cbnpboutill
2012-12-21Awful heuristic to refold mutual fixpoint in reductionopspboutill
2012-12-21Fixup and comment reductionopspboutill
2012-12-19Reductionops reduction machine can refold constantpboutill
2012-12-19Evarconv.Pseudorigid erasurepboutill
2012-12-19Coqide: cleaner Coq.PrintOpt and session creationletouzey
2012-12-19Array.create is deprecatedpboutill
2012-12-19GtkData.set_default_modifiers and no access to <primary> in lablgtk -> unsuab...pboutill
2012-12-19Fix coqtop -config when absolute path have been given for ocaml*pboutill
2012-12-18Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)letouzey
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-18Fixing parsing of specific primitive tokens used as notations for patternsherbelin
2012-12-18Taking into account the possibility of having a type of type which isherbelin
2012-12-18Extraction: qualified names in Extract Constant examples (fix #2878)letouzey
2012-12-18No more constant named "int" in Coq theories (cf bug #2878)letouzey
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
2012-12-18Factorization of the elim unif flag with the default flag. Sinceherbelin
2012-12-17Fixed interpretation of "x" as a binding variable for the returnherbelin
2012-12-17Do not display REVERTcast inserted by reduction tactics (unless printing all).herbelin
2012-12-17Fixed a bug in the algorithm trying to elaborate a "match" return predicate.herbelin
2012-12-17Ide_slave: do not prepare debug messages in non-debug modeletouzey
2012-12-17Extraction of projections: restrict a hack to ocaml only (fix #2941)letouzey
2012-12-14Fixing ocalmdoc commentppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Fixing CoqIDE compilationppedrot
2012-12-14Moving hcons_string to String namespace.ppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
2012-12-13Using library string functions.ppedrot
2012-12-13Documented CString.ppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-12-11Wg_ScriptView: avoid invalid iters during completionletouzey
2012-12-11Coqide: allow editing even during a backtrackletouzey
2012-12-11Coq_lex: direct accounting of utf8 extra bytes in offsetsletouzey
2012-12-10Coqide: restore the tag removal of copy-pasted zonesletouzey
2012-12-10Coqide: some more refactoring to lighten coqide.mlletouzey
2012-12-10Coq_makefile: Better rule for subdirs when the subdir does not existpboutill
2012-12-10Tiny fix of r16049pboutill
2012-12-10* Implementing the "union by rank" optimisation in univ.mlpboutill
2012-12-08Ensure that a function declared with a label is used with itletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 18:12:51 +0000