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
*
Avoid registering λ and Π as keywords just for some private Local Notation
letouzey
2011-09-06
*
ide/preferences.ml: apparently no `META in Gdk.Tags.modifier
letouzey
2011-09-06
*
Ocamlbuild : build of fake_ide
letouzey
2011-09-06
*
fake_ide: a short program to mimic an ide talking to coqtop -ideslave
letouzey
2011-09-05
*
Coqide: new backtracking code, based on the Backtrack command
letouzey
2011-09-05
*
Ide_intf: slight reorganisation of the IDE api
letouzey
2011-09-05
*
Lib: remove strange code about backtracking to the current state
letouzey
2011-09-05
*
Lib.node: merge OpenedModtype and OpenedModule, same for Closed...
letouzey
2011-09-05
*
Remove code concerning the obsolete Set/Unset Undo
letouzey
2011-09-05
*
Util.error now creates UserError(_,msg) instead of UserError(str,str)
letouzey
2011-09-05
*
Extraction Implicit: fix the numbering of constructor arguments
letouzey
2011-09-05
*
Having added a special Cast for remembering the use of conversion
herbelin
2011-09-04
*
Bug 3596: ocamlbuild: coq_makefile now requires Unix
pboutill
2011-09-03
*
Bug 2589: Documentation patch of Hendrik Tews
pboutill
2011-09-02
*
Coq_makefile: bugfix in install rule
pboutill
2011-09-02
*
Automatic search of project file
pboutill
2011-09-01
*
Coq_makefile : bug when a project file is not in the current directory.
pboutill
2011-09-01
*
safe_prerr_endline in Minilib
pboutill
2011-09-01
*
Add option -f to coqide
pboutill
2011-09-01
*
Add preferences to say how to deal with a project file.
pboutill
2011-09-01
*
same_file in Minilib
pboutill
2011-09-01
*
load_file takes advantage of same_file optimisation
pboutill
2011-09-01
*
create_session takes the filename as argument.
pboutill
2011-09-01
*
No more parser for reading coqide pref file
pboutill
2011-09-01
*
[/]+ is equivalent to [/] in System and its copy
pboutill
2011-09-01
*
Coq_makefile.absolute_dir -> Minilib.canonical_path_name
pboutill
2011-09-01
*
Creation of ide/project_file.ml4
pboutill
2011-09-01
*
gitignore update
pboutill
2011-09-01
*
Coq_makefile: Bug fix of check_dep
pboutill
2011-09-01
*
Coq_makefile: process_cmd_line is purely functional.
pboutill
2011-09-01
*
Coq_makefile: No other function than split_arguments uses a target type.
pboutill
2011-09-01
*
Coq_makefile: New option -arg to specify a compiler option.
pboutill
2011-09-01
*
Coq_makefile drops the '/' at the end of physical path of -I and -R
pboutill
2011-09-01
*
Several bug reports came from confusions between generalize and set.
pboutill
2011-09-01
*
Bug 2583: Update of the syntax of terms in the reference manual
pboutill
2011-09-01
*
Bug 2577: Second attempt to be correct.
pboutill
2011-09-01
*
Porting Hendrik's 8.3 patch for proof tree visualization under proof
herbelin
2011-08-30
*
Quick improvement of some error messages related to module application
herbelin
2011-08-30
*
Extraction: allow extraction of records with anonymous fields (fix #2555)
letouzey
2011-08-25
*
Use of the standard terminology for Diaconescu's theorem (not "paradox").
herbelin
2011-08-23
*
Clarifying that only identifiers are advertised to be turned into keywords
herbelin
2011-08-23
*
Tactics.compute_scheme_signature: factorize the two almost-similar cases
letouzey
2011-08-22
*
Updates in CHANGES
letouzey
2011-08-18
*
Remove old file (1999)
msozeau
2011-08-18
*
Misc improvements concerning "Show Match" and its coqide equivalent
letouzey
2011-08-18
*
Give inner fixpoint of gcd31 a name, to avoid excessive unfolding
glondu
2011-08-17
*
Smaller proof terms for QcPower_{0,pos}
glondu
2011-08-17
*
Fixes bug #2587 (Print Hint gives anomaly when no focused subgoals)
aspiwack
2011-08-16
*
New fix for is_ident_not_keyword.
herbelin
2011-08-13
*
Fixes mini-bug: Qed would succeed even on focused proofs.
aspiwack
2011-08-12
[next]