aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2012-12-07Coqide: minor cleanup around tag_on_insertletouzey
2012-12-07Coqide: better removal of the error red tagletouzey
2012-12-07Coqide: better handling of gtk messages + fix win32 stdout/stderr reroutingletouzey
2012-12-07Coqide: no reason to ignore Ctrl-Cletouzey
2012-12-07Coqide: use "prefs" ident instead of "current" (vague when unqualified)letouzey
2012-12-07Coqide: opening non-existing files won't create them immediately anymoreletouzey
2012-12-07Coqide: nicer creation of timersletouzey
2012-12-07Coqide: code cleanupletouzey
2012-12-07* lib/Envars:regisgia
2012-12-07* lib/Envars:regisgia
2012-12-07Revert "* tools/Coq_makefile:"regisgia
2012-12-07* tools/Coq_makefileregisgia
2012-12-07* tools/Coq_makefile:regisgia
2012-12-06Restoring flush of Welcome message lost in r15148herbelin
2012-12-05Making subset_eq_compat applying over more general domain "Type" (see #2938).herbelin
2012-12-04Backtrack on activating scopes with type casts (was r15978).herbelin
2012-12-04Removed Compat.Exc_located outside of compat.ml4, as a consequence ofherbelin
2012-12-04Early translation of camlp4/camlp5 located errors into coq-locatedherbelin
2012-12-04Low-level hack to get some more informative message from dynamic loading errors.herbelin
2012-12-04Fixing a comment.herbelin
2012-12-04Revised the strategy for automatic insertion of spaces when printingherbelin
2012-12-04Display Menu now called View Menu (in CoqIDE preferences).herbelin
2012-12-04Identities over types satisfying Uniqueness of Identity Proofsherbelin
2012-12-04Coqmktop: use the atomic Filename.open_temp_fileletouzey
2012-11-28Evarconv: Fix #2936 + commentspboutill
2012-11-28Fix ocamldebug constr printerpboutill
2012-11-28Reductionops uses Closure.redspboutill
2012-11-28Kernel/closure: add eta red_kindpboutill
2012-11-26Removed some FIXME related to equality on universes.ppedrot
2012-11-26Small cleaning of interface in Univppedrot
2012-11-26Monomorphization (toplevel)ppedrot
2012-11-26Fixed a monomorphization error.ppedrot
2012-11-25Monomorphization (tactics)ppedrot
2012-11-25Monomorphization (proof)ppedrot
2012-11-25Monomorphization (library)ppedrot
2012-11-25Monomorphization (parsing)ppedrot
2012-11-25Monomorphization (interp)ppedrot
2012-11-25More equality functionsppedrot
2012-11-25Fixed bug #2930: folded let-in's were hiding a violation to the occurherbelin
2012-11-23Added a constr_pattern_eqppedrot
2012-11-22Monomorphization (pretyping)ppedrot
2012-11-22Monomorphization (library)ppedrot
2012-11-22Monomorphization (kernel)ppedrot
2012-11-22Monomorphization (lib)ppedrot
2012-11-21Fixing test-suite: Scope.vppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-04 19:14:42 +0000