index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
Commit message (
Expand
)
Author
Age
...
*
|
|
|
|
Removing constr generic argument.
Pierre-Marie Pédrot
2016-01-14
*
|
|
|
|
Removing ident and var generic arguments.
Pierre-Marie Pédrot
2016-01-14
*
|
|
|
|
CLEANUP: removing unused field
Matej Kosik
2016-01-11
*
|
|
|
|
merge
Matej Kosik
2016-01-11
|
\
\
\
\
\
|
*
|
|
|
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
|
|
|
Use streams rather than strings to handle bullet suggestions.
Guillaume Melquiond
2016-01-02
*
|
|
|
|
|
Remove some unused functions.
Guillaume Melquiond
2016-01-02
*
|
|
|
|
|
Reduce dependencies of interface files.
Guillaume Melquiond
2016-01-02
*
|
|
|
|
|
Remove useless rec flags.
Guillaume Melquiond
2016-01-02
*
|
|
|
|
|
Simplification of grammar_prod_item type.
Pierre-Marie Pédrot
2016-01-02
*
|
|
|
|
|
Separation of concern in TacAlias API.
Pierre-Marie Pédrot
2016-01-02
*
|
|
|
|
|
Do not compose List.length with List.filter.
Guillaume Melquiond
2015-12-31
*
|
|
|
|
|
External tactics and notations now accept any tactic argument.
Pierre-Marie Pédrot
2015-12-30
*
|
|
|
|
|
Removing the special status of open_constr generic argument.
Pierre-Marie Pédrot
2015-12-28
*
|
|
|
|
|
Tentative API fix for tactic arguments to be fed to tclWITHHOLES.
Pierre-Marie Pédrot
2015-12-27
*
|
|
|
|
|
Removing auto from the tactic AST.
Pierre-Marie Pédrot
2015-12-24
*
|
|
|
|
|
Do not compose "str" and "to_string" whenever possible.
Guillaume Melquiond
2015-12-22
*
|
|
|
|
|
Removing ad-hoc interpretation rules for tactic notations and their genarg.
Pierre-Marie Pédrot
2015-12-21
*
|
|
|
|
|
Changing the toplevel type of the int_or_var generic type to int.
Pierre-Marie Pédrot
2015-12-21
*
|
|
|
|
|
Removing the now useless genarg generic argument.
Pierre-Marie Pédrot
2015-12-21
*
|
|
|
|
|
Using dynamic values in tactic evaluation.
Pierre-Marie Pédrot
2015-12-21
|
/
/
/
/
/
*
|
|
|
|
CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified
Matej Kosik
2015-12-18
*
|
|
|
|
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
Matej Kosik
2015-12-18
*
|
|
|
|
CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...
Matej Kosik
2015-12-18
*
|
|
|
|
CLEANUP: Vernacexpr.vernac_expr
Matej Kosik
2015-12-18
*
|
|
|
|
Tying the loop in tactic printing API.
Pierre-Marie Pédrot
2015-12-18
*
|
|
|
|
Getting rid of some hardwired generic arguments.
Pierre-Marie Pédrot
2015-12-17
*
|
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
|
|
*
|
|
|
|
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-12-05
*
|
|
|
|
Getting rid of the dynamic node of the tactic AST.
Pierre-Marie Pédrot
2015-12-04
*
|
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
\
\
\
\
|
|
*
|
|
|
Improving over printing of let-tuple (see #4447).
Hugo Herbelin
2015-12-03
|
|
/
/
/
/
|
*
|
|
|
Dead code from August 2014 in apply in.
Hugo Herbelin
2015-12-02
*
|
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
|
|
|
*
|
|
|
Adding syntax "Show id" to show goal named id (shelved or not).
Hugo Herbelin
2015-11-02
|
|
*
|
|
Make the code of compare functions linear in the number of constructors.
Arnaud Spiwack
2015-10-29
*
|
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
|
|
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Univs: local names handling.
Matthieu Sozeau
2015-10-28
|
*
|
|
Printing of @{} instances for polymorphic references in Print and About.
Matthieu Sozeau
2015-10-28
*
|
|
|
Type delayed_open_constr is now monotonic.
Pierre-Marie Pédrot
2015-10-19
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
|
|
*
|
|
Axioms now support the universe binding syntax.
Pierre-Marie Pédrot
2015-10-08
|
*
|
|
Goptions: new value type: optional string
Enrico Tassi
2015-10-08
|
*
|
|
Univs: add Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-10-07
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-06
|
\
|
|
|
|
*
|
|
Univs: fix printing bug #3797.
Matthieu Sozeau
2015-10-05
|
|
|
*
Show assumptions of well-foundedness in `Print Assumptions`
Arnaud Spiwack
2015-09-25
*
|
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-25
|
\
|
|
|
|
|
|
*
Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...
Arnaud Spiwack
2015-09-25
|
*
|
|
Print Assumptions shows engagement.
Maxime Dénès
2015-09-20
[prev]
[next]