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
*
Fixed "Eval ... in t" when t has still metavariables.
herbelin
2011-04-08
*
Fixing multiple printing bugs with "Notation f x := ..."
herbelin
2011-04-08
*
Extraction: unfolds the let-in created by Program when handling "match"
letouzey
2011-04-07
*
Extraction: avoid some useless Obj.magic by fixing my ML type unifier
letouzey
2011-04-07
*
Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)
herbelin
2011-04-06
*
A few extra combinators about rel_declaration/named_declaration + a bit of doc
herbelin
2011-04-06
*
Fix dev/base_include after change of constant_body
letouzey
2011-04-06
*
Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.
aspiwack
2011-04-06
*
Add 'Existing Instances' declaration to declare multiple instances at once.
letouzey
2011-04-06
*
Update documentation concerning proofs loading (cf last commit)
letouzey
2011-04-03
*
Fix last commit about coqdep: not everyone has a user-contrib dir
letouzey
2011-04-03
*
Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks
letouzey
2011-04-03
*
Quickly avoid global axioms in Loic new files about ring
letouzey
2011-04-03
*
Adjust coqdep so that it behaves like coqtop with respect to the user-contrib...
gmelquio
2011-04-01
*
CHANGES: a word about recent changes in coqide, about Ctrl-C in vm
letouzey
2011-04-01
*
Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)
letouzey
2011-04-01
*
Did that adding a rule for printing applications as "f(x)" works.
herbelin
2011-03-31
*
As remarked by Enrico, we'd better use eq_constr than structural equality
herbelin
2011-03-31
*
Extraction: customized inductives are always standard
glondu
2011-03-31
*
Cyclic: a small optimisation with nice effect on BigN.mul (thinks Benjamin)
letouzey
2011-03-30
*
Coqide: avoid confusion of process when restarting coqtop + cosmetic
letouzey
2011-03-30
*
Ide_intf: documentation of calls + debug printing of calls/answers
letouzey
2011-03-30
*
Ide_intf: remove useless int answer to the "interp" and "rewind" calls
letouzey
2011-03-30
*
Ide_slave: better handling of Ctrl-C
letouzey
2011-03-30
*
Coqide: synchronise the reset_initial via the coq_computing mutex
letouzey
2011-03-30
*
Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_break
letouzey
2011-03-28
*
Ide: restaure compilation of ide/macjokes.c removed by mistake
letouzey
2011-03-28
*
Ide: misc (nicer message than End_of_file, a useless try removed
letouzey
2011-03-28
*
Ide_slave: improved handling of exceptions (in particular ^C)
letouzey
2011-03-28
*
Ide_slave: a more robust current_status () function
letouzey
2011-03-28
*
Ide: new option -coqtop <mycoqtop> + remove wrong quoting of args
letouzey
2011-03-28
*
ide/coqide.ml: a pass of more decent automatic indentation
letouzey
2011-03-25
*
Ide: more reorganisation and cleanup
letouzey
2011-03-25
*
Ide_intf : change type of location in ide
letouzey
2011-03-25
*
Ide: mention "Restart" instead of "Go to start" for corresponding button
letouzey
2011-03-25
*
Ide: stronger separation from coqtop
letouzey
2011-03-23
*
Ide: experimentally allow coqide to interrupt or kill coqtop
letouzey
2011-03-23
*
- Remove useless grammar rule
msozeau
2011-03-23
*
- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...
msozeau
2011-03-23
*
Documentation of the timeout tactical (cf r13917)
letouzey
2011-03-21
*
Init: some results in Type should rather be Defined than Qed
letouzey
2011-03-21
*
Makefile.build: states/initial.coq was wrongly done with -dont-load-proofs
letouzey
2011-03-21
*
Makefile.build: compile the stdlib with -dont-load-proofs by default
letouzey
2011-03-18
*
A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds
letouzey
2011-03-18
*
An option "Set Default Timeout n."
letouzey
2011-03-17
*
Goptions: repair Unset for int options
letouzey
2011-03-17
*
CompareSpec: a slight generalization/reformulation of CompSpec
letouzey
2011-03-17
*
Adapt printers.mllib after my last commit
letouzey
2011-03-16
*
Finish branching functions handling module errors (cf. r13886)
letouzey
2011-03-16
*
Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)
letouzey
2011-03-16
[next]