aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-12-08Finish patch for Hint Resolve, stopping to generate new constant names formsozeau
2012-12-08Coqide: use labels for all labelled functionsletouzey
2012-12-08Coqide: handle possible fragmentation in xml answersletouzey
2012-12-08Coqide: get rid of threads, use gtk asynchronous i/o insteadletouzey
2012-12-08Removed a unused function in Ppppedrot
2012-12-08Small optimization in Closure: replaced an index list with an array.ppedrot
2012-12-07Coqide: more cleanup (buffers)letouzey
2012-12-07Coqide: stylistic improvements in analyzed_view initializerletouzey
2012-12-07Coqide: cleanup concerning insert_text signalletouzey
2012-12-07Nicer code around Coq_lexletouzey
2012-12-07Ideutils: simpler conversion from byte offset to utf8 char offsetletouzey
2012-12-07Coqide: missing arg when calling process_next_phraseletouzey
2012-12-07Envars: repair failed compilation after yann's commitsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 16:07:55 +0000