index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
Cleaning debugging printer relative to new proof engine. In
herbelin
2011-06-21
*
Add compatibility option "-compat 8.3".
herbelin
2011-06-20
*
Relaxed the constraint introduced in r14190 that froze the existing
herbelin
2011-06-18
*
Fixing bug #2181 (Class mechanism can create dependencies over unnamed
herbelin
2011-06-14
*
Another bug of Scheme Induction (generated names dep/nodep were swapped).
herbelin
2011-06-13
*
Fixing an anomaly in Scheme Induction.
herbelin
2011-06-13
*
Made the emacs-U option deprecated. Also removed the old code
courtieu
2011-05-24
*
Coqide: allow the use of Abort (grant wish #2357)
letouzey
2011-05-18
*
More work on error handling
letouzey
2011-05-17
*
Break circular dependency Proof_global -> Vernacexpr -> Proof_global.
aspiwack
2011-05-17
*
Repair the "Fail" command after recent changes in exception handling
letouzey
2011-05-16
*
turn the automatic generation of boolean equality
vsiles
2011-05-16
*
Turning Sys_error into error by default instead of anomaly. After all,
herbelin
2011-05-15
*
A new mechanism to handle errors.
aspiwack
2011-05-13
*
New option [Set Bullet Behavior] allows to select the behaviour of bullets.
aspiwack
2011-05-13
*
Print Module (Type) M now tries to print more details
letouzey
2011-05-11
*
Merge branch 'subclasses' into coq-trunk
msozeau
2011-05-05
*
Fixed a bug causing inconsistent states during proof editting.
aspiwack
2011-04-29
*
coqtop -config returns coq returns coq environments at exection time
pboutill
2011-04-28
*
Fixed notation printing bug when curly brackets are involved (requests
herbelin
2011-04-28
*
Coqide: better handling of stdout/stderr in win32
letouzey
2011-04-21
*
Add a flag to control betaiota reduction during unification to maintain backw...
msozeau
2011-04-18
*
Add directories in COQPATH to search path.
herbelin
2011-04-14
*
Reorder search path order, so the standard library is search last.
herbelin
2011-04-14
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
- Make typeclass transparency information directly available
msozeau
2011-04-13
*
- Remove create_evar_defs
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Replaced printing number of ill-typed branch by printing name of constructor
herbelin
2011-04-08
*
Fixed "Eval ... in t" when t has still metavariables.
herbelin
2011-04-08
*
Add 'Existing Instances' declaration to declare multiple instances at once.
letouzey
2011-04-06
*
Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks
letouzey
2011-04-03
*
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
*
Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_break
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_intf : change type of location in ide
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
*
- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...
msozeau
2011-03-23
*
An option "Set Default Timeout n."
letouzey
2011-03-17
*
Goptions: repair Unset for int options
letouzey
2011-03-17
*
Finish branching functions handling module errors (cf. r13886)
letouzey
2011-03-16
*
- Add modulo_delta_types flag for unification to allow full
msozeau
2011-03-13
*
Keep information on which fields are subclasses in class declarations,
msozeau
2011-03-11
*
- Better error messages taking unif. constraints into account.
msozeau
2011-03-11
*
Reverted commit r13893 about propagation of more informative
herbelin
2011-03-07
*
Added propagation of evars unification failure reasons for better
herbelin
2011-03-07
[next]