index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2011-12-06
Documentation for Arguments + simpl
gareuselesinge
2011-12-06
Minor fixes to Arguments
gareuselesinge
2011-12-06
Backtrack on synchronizing universe counter with reset
herbelin
2011-12-05
Registering universe and meta/evar counters as summaries so as to
herbelin
2011-12-05
Yet another fix about alias in testing if pattern unification applies.
herbelin
2011-12-04
Fixing bugs in doc about when "with" is needed or not to give bindings
herbelin
2011-12-04
Fixed a small regression in pattern-matching compilation introduced in
herbelin
2011-12-04
A small test for type inference (used to be a regression at some time).
herbelin
2011-12-04
Fixing superflous newline in output of About when no parameter is renamed.
herbelin
2011-12-04
Discarding let-ins from the instances of the evars in the
herbelin
2011-11-30
Fixed a bug introduced in r12755. CoqIDE would ignore the Printing Existentia...
ppedrot
2011-11-30
Extraction: try to avoid issues with an Include directly inside a .v
letouzey
2011-11-30
Now CoqIDE relies on the option query mechanism to set printing options. Stil...
ppedrot
2011-11-30
More type safety in query GADT (again).
ppedrot
2011-11-30
Fixed a serious bug in XML marshalling due to unsafe GADTs. Now types are enf...
ppedrot
2011-11-30
Continuing r14747 being actually incomplete (flushing warnings and
herbelin
2011-11-30
Quick hack to avoid anomaly on using Program w/o having required JMeq.
herbelin
2011-11-30
Preventing Implicit Arguments warning to be shown in non verbose mode
herbelin
2011-11-29
Documentation of appcontext
letouzey
2011-11-29
Fixed a warning about unused variable introduced in r14731
ppedrot
2011-11-29
lib/xml_lexer.ml in .gitignore (produced by a .mll)
letouzey
2011-11-29
Extraction: typo in last commit
letouzey
2011-11-29
fix for bug #2649
corbinea
2011-11-29
Term: properly ignore Casts between Apps in constr_ord
puech
2011-11-29
Term: useless conversion to list in constr_ord deleted
puech
2011-11-28
Finally used typing to decide whether an alias needs to be expanded or
herbelin
2011-11-28
Fixing dependencies postprocessing bug in pattern-matching compilation.
herbelin
2011-11-28
Term: Fix hash_constr behavior for Cast lnterleaved in application spines.
puech
2011-11-28
Extraction: Richer patterns in matchs as proposed by P.N. Tollitte
letouzey
2011-11-28
doc: two minor fixes to make my latex happy
letouzey
2011-11-26
Fixed a bug in postprocessing dependencies in pattern-matching compilation
herbelin
2011-11-25
Added an API call to retrieve and change the option state
ppedrot
2011-11-25
Separated the toplevel interface into a purely declarative module with associ...
ppedrot
2011-11-25
Cleaning up XML parsing
ppedrot
2011-11-25
avoid relying on weak invariant in cbv.ml
bgregoir
2011-11-24
Added a function to inspect current option state.
ppedrot
2011-11-24
Fixed the XML parser CDATA handling (and changed the EOL convention of these ...
ppedrot
2011-11-24
Fixed some missing options from previous commit.
ppedrot
2011-11-24
Added a DEPRECATED flag in declaration of options. For now only two options a...
ppedrot
2011-11-24
Moving XML handling to lib directory
ppedrot
2011-11-24
Correct direction for definitional typeclasses
msozeau
2011-11-23
In emacs mode, prints a list of the dependent existential variables introduced
aspiwack
2011-11-23
Adds a pair of function in Evar_util to gather dependent evars in an
aspiwack
2011-11-21
Renamig support added to "Arguments"
gareuselesinge
2011-11-21
theories/, plugins/ and test-suite/ ported to the Arguments vernacular
gareuselesinge
2011-11-21
New Arguments vernacular
gareuselesinge
2011-11-21
Configurable simpl tactic
gareuselesinge
2011-11-21
coqide default pref files are by default in /etc/xdg/coq/
pboutill
2011-11-21
/home/pirbo/.coqrc* are read again
pboutill
2011-11-21
-user option removal
pboutill
[next]