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
...
|
|
|
|
*
|
|
|
A first step at refreshing and documenting the new feature.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Adding support for parsing subterms of a notation as "pattern".
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Adding patterns in the category of binders for notations.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Preliminary work before adding general support for patterns in notations II.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Preliminary work before adding general support for patterns in notations I.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Preliminary work before extending support for binders in notations
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Preliminary steps before adding general support for patterns in notations.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
In printing notations with "match", reasoning up to the order of clauses.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Preliminary work before extending support for binders in notations
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Make pattern variables of "match" substitutable in notations.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Supporting recursive notations reversing the left-to-right order.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Allowing variables used in recursive notation to occur several times in pattern.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Allows recursive patterns for binders to be associative on the left.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Fixing/improving notations with recursive patterns.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
A bit of miscellaneous code documentation around notations.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Notations: documenting structure collecting variables occurring in notation.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Renaming binders into binderlists in egramcoq.ml.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Introducing an intermediary type "constr_prod_entry_key" for grammar producti...
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Canonically add an encoding in glob_constr of "as" operator for cases_pattern.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Minor clarifying of name variables in constrintern.ml.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Using name given by user to name a 'pat, if any.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Notations: Do not consider a non-occurring variable as a binder-only variable.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
More precise explanation when a notation is not reversible for printing.
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Adding support for re-folding notation referring to isolated "forall '(x,y), t".
Hugo Herbelin
2018-02-20
|
|
|
|
*
|
|
|
Again one more step in fixing #5762 ("where" clause).
Hugo Herbelin
2018-02-20
|
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
ci: add elpi
Enrico Tassi
2018-02-19
|
|
|
|
*
|
|
record: restore API declare_projections (removed in e414c07e1)
Enrico Tassi
2018-02-19
|
|
|
|
*
|
|
pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)
Enrico Tassi
2018-02-19
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6761: Remove unused argument in Record.declare_structure
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #6753: [toplevel] Make toplevel state into a record.
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
*
|
|
|
Fix #6529: nf_evar_info and check the env evars' not just the concl
Matthieu Sozeau
2018-02-19
*
|
|
|
|
|
|
|
|
|
Merge PR #6230: Better Cemitcodes API + compact relocation representation
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #6759: detype_case predicate is not optional
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6772: Cleanup inferCumulativity
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6648: [tactics] make apply_type safe
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds.
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6571: Fix ci-all target
Maxime Dénès
2018-02-19
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
\
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
|
|
|
Change references to CAMLP4 to CAMLP5 to be more accurate since we no
Jim Fehrle
2018-02-17
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
|
|
apply_type: add option "typecheck" passed down to refine
Enrico Tassi
2018-02-16
|
|
_
|
_
|
_
|
/
/
/
/
/
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
|
Cleaner treatment of parameters in inferCumulativity
Gaëtan Gilbert
2018-02-16
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
|
Fix reduction flags in inferCumulativity
Gaëtan Gilbert
2018-02-16
|
|
_
|
_
|
_
|
/
/
/
/
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
Adding a test for the construction that was broken in Coccinelle.
Pierre-Marie Pédrot
2018-02-16
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
Extrude monomorphic universe contexts from with Definition constraints.
Pierre-Marie Pédrot
2018-02-16
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
Adding a test for variance subtyping in the module system.
Pierre-Marie Pédrot
2018-02-15
[prev]
[next]
Hugo Herbelin
Enrico Tassi
Maxime Dénès
Matthieu Sozeau
Jim Fehrle
Gaëtan Gilbert
Pierre-Marie Pédrot