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
...
*
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
*
Added a table for using reserved names for binding names to types
herbelin
2011-03-05
*
Moving printing of module typing errors upwards to himsg.ml so as to
herbelin
2011-03-05
*
A few more betaiota on environments and types of error messages. Seems to
herbelin
2011-03-05
*
Filter out admitted subgoals from search results
glondu
2011-02-25
*
- Fix treatment of globality flag for typeclass instance hints (they
msozeau
2011-02-14
*
An automatic substitution of scope at functor application
letouzey
2011-02-11
*
Annotations at functor applications:
letouzey
2011-02-11
*
Remove obsolete TheoryList
glondu
2011-02-10
*
Fixpoints are traverse during implicits arguments search to toplevel
pboutill
2011-02-10
*
Interp a definition with the implicit arguments of its local context
pboutill
2011-02-10
*
Data structure telling implicits of local variables is a map in the
pboutill
2011-02-10
*
More comments and less doublons in some mli
pboutill
2011-02-10
*
Started to fix the declarative proof mode (C-zar).
aspiwack
2011-02-10
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Add "Print Sorted Universes"
glondu
2011-01-11
*
Use dashed lines for equivalence edges in dot output of universes
glondu
2011-01-11
*
Reverted r13715 "Add improved indenters that rely on the current proof state ...
gmelquio
2011-01-06
*
Remove Safe_marshal
glondu
2011-01-06
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Misc improvements about evar_map
letouzey
2010-12-15
*
Add improved indenters that rely on the current proof state to choose the ind...
gmelquio
2010-12-14
*
First release of Vector library.
pboutill
2010-12-10
*
Fixing bug using explictly declared implicit arguments in inductive arities.
herbelin
2010-12-03
*
Redirect stdout to stderr in -ideslave
glondu
2010-12-03
*
Fixing a bug introduced in r12304 (move of interpretation of
herbelin
2010-12-02
*
Do not throw an error for anonymous generalized binders as they will be
msozeau
2010-11-18
*
Remove redundant clause (and fix compatibility issue)
glondu
2010-11-16
*
Minor fixes from Gregory Malecha. A typo fixed and a better (located)
msozeau
2010-11-15
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
Add information of localisation when an error involving an "implicit
herbelin
2010-11-07
*
correcting a non catch error reported as an anomaly (Ploc.Exc)
jforest
2010-11-07
*
In Univ, unify order_request and constraint_type
glondu
2010-11-03
[prev]
[next]