index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
New module Xml_printer (dual to Xml_parser)
gareuselesinge
2013-05-06
*
Coqide: view -> zoom in / out / fit
gareuselesinge
2013-05-06
*
States: frozen states can hold closures
gareuselesinge
2013-05-06
*
Summary: support selective freeze
gareuselesinge
2013-05-06
*
Ideutils: comment on missing Glib utf8 handling function
gareuselesinge
2013-05-06
*
Close the .glob file after having saved .vo
gareuselesinge
2013-05-06
*
Fix typo in manual
gareuselesinge
2013-05-06
*
Improving printing of 'rew' notation
herbelin
2013-05-05
*
Hack to solve a "Bad recursive type" anomaly.
herbelin
2013-05-05
*
Now printing body of abbreviations (i.e. notation with a name) with
herbelin
2013-05-05
*
Little fix for Nsatz: hypotheses not directly relevant to the nsatz
herbelin
2013-05-05
*
Improvement of r16204 on reporting tactic error locations: if the main
herbelin
2013-05-05
*
Relaxing the constraint on eta-expanding on the fly while looking for
herbelin
2013-05-05
*
Reporting the change on matching partial applications in patterns of
herbelin
2013-05-05
*
Removing a redundant function from Evd.
ppedrot
2013-05-03
*
Fix wrong computation of dependency signature in cases raising an uncaught ex...
msozeau
2013-04-30
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Added a unit test for bug #2230.
ppedrot
2013-04-27
*
Fix compilation (vernac.ml, missing ;)
gareuselesinge
2013-04-25
*
Fix: tooltip correctly handles the absence of info (empty string)
gareuselesinge
2013-04-25
*
Coqide: Globalization feedback (proof of concept)
gareuselesinge
2013-04-25
*
lablgtk2 misses Glib.Utf8.pos_to_offset, workaround in ideutils
gareuselesinge
2013-04-25
*
Flag ide_slave moved into Flags module
gareuselesinge
2013-04-25
*
Coqide: new tag "tooltip" for the Script window
gareuselesinge
2013-04-25
*
raise UnsafeSuccess -> feedback AddedAxiom
gareuselesinge
2013-04-25
*
Coqide: new feedback mechanism for structured content
gareuselesinge
2013-04-25
*
Fix indentation
gareuselesinge
2013-04-25
*
Fix issues with "Reset Initial" in scripts given to coqtop -l
letouzey
2013-04-23
*
Egramcoq+Lexer : no need for an init_function
letouzey
2013-04-23
*
Indfun : use States.with_state_protection instead of freeze/unfreeze
letouzey
2013-04-23
*
Egramcoq: clean an ugly code snippet
letouzey
2013-04-23
*
minor cleanup in coqtop.ml
letouzey
2013-04-23
*
coqtop -compile: avoid with_heavy_rollback when non-interactive
letouzey
2013-04-23
*
Coqtop -compile : avoid saving init state when compiling just one file
letouzey
2013-04-23
*
Remove deprecated option -no-hash-consing (currently doing nothing)
letouzey
2013-04-23
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Declaremods: some more minor cleanup
letouzey
2013-04-22
*
Fix compilation of fake_ide
gareuselesinge
2013-04-19
*
interface.mli and serialize.ml reworked to avoid copy/paste of types
gareuselesinge
2013-04-19
*
coqc and coqmktop migrated in tools/, get rid of scripts/ subdir
letouzey
2013-04-18
*
Coqdep: add an -exclude-dir option (wish mentionned in #3025)
letouzey
2013-04-18
*
Coqc: accept -exclude-dir + some others + cleanup (fix #3025)
letouzey
2013-04-18
*
Finer fix for bug 3017, mark unresolvability only of goals that are
msozeau
2013-04-18
*
Only arguments declared as implicit can be renamed
gareuselesinge
2013-04-18
*
Fix #3001 (rename arg of global cst inside section)
gareuselesinge
2013-04-18
*
Renaming SearchAbout into Search and Search into SearchHead.
herbelin
2013-04-17
*
Matching patterns: fixed allow_partial_app which was not working on
herbelin
2013-04-17
*
Fix of r16257 in r16205 for "errors raised by check_evar_instance were
herbelin
2013-04-17
*
Coqmktop: dynlink is now mandatory due to Maxime's native-compiler
letouzey
2013-04-17
[next]