index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
Commit message (
Expand
)
Author
Age
*
Merge PR #7620: [ssr] rewrite: turn anomaly into regular error
Maxime Dénès
2018-06-25
|
\
*
\
Merge PR #7236: [ssr] simpler semantics for delayed clears
Maxime Dénès
2018-06-23
|
\
\
*
|
|
Using more general information for primitive records.
Pierre-Marie Pédrot
2018-06-23
*
|
|
Change the proj_ind field from MutInd.t to inductive.
Pierre-Marie Pédrot
2018-06-23
|
*
|
[ssr] implement {}/v as a short hand for {v}/v when v is an id
Enrico Tassi
2018-06-22
|
*
|
[ssr] simplify delayed clears
Enrico Tassi
2018-06-22
*
|
|
[ssr] matching: use eq_constr_nounivs in approximated matching
Enrico Tassi
2018-06-22
*
|
|
[ssr] set: merge universe constraints before type checking the term
Enrico Tassi
2018-06-22
|
/
/
|
*
[ssr] rewrite: turn anomaly into regular error
Enrico Tassi
2018-06-20
|
/
*
Merge PR #7797: Remove reference name type.
Enrico Tassi
2018-06-19
|
\
*
\
Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.
Pierre-Marie Pédrot
2018-06-19
|
\
\
|
*
|
Fix #7421: constr_eq ignores universe constraints.
Gaëtan Gilbert
2018-06-18
|
|
*
Remove reference name type.
Maxime Dénès
2018-06-18
|
|
/
*
|
Remove the proj_body field from the kernel.
Pierre-Marie Pédrot
2018-06-17
*
|
Getting rid of the const_proj field in the kernel.
Pierre-Marie Pédrot
2018-06-17
|
/
*
Workaround to handle non-value arguments in tactics.
Cyprien Mangin
2018-06-14
*
[api] Remove Misctypes.
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Misctypes removal: move Tactypes to proofs
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Misctypes removal: multi to tactics/rewrite
Emilio Jesus Gallego Arias
2018-06-12
*
Micromega clean-up
Maxime Dénès
2018-06-07
*
Make direct invocations of `simple apply` obey `Opaque` directive.
Maxime Dénès
2018-06-05
*
Merge PR #7229: Deprecate implicit tactic solving.
Hugo Herbelin
2018-06-04
|
\
*
\
Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-
Pierre-Marie Pédrot
2018-06-04
|
\
\
*
\
\
Merge PR #7216: Replace uses of Termops.dependent by more specific functions.
Matthieu Sozeau
2018-06-04
|
\
\
\
|
|
|
*
Deprecate implicit tactic solving.
Pierre-Marie Pédrot
2018-06-04
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #7234: Reduce circular dependency constants <-> projections
Maxime Dénès
2018-06-01
|
\
\
\
|
|
|
*
Refactor parsing rules for Hint Resolve -> and Hint Resolve <-
Armaël Guéneau
2018-05-31
*
|
|
|
[notations] Split interpretation and parsing of notations
Emilio Jesus Gallego Arias
2018-05-31
*
|
|
|
[api] Move `Constrexpr` to the `interp` module.
Emilio Jesus Gallego Arias
2018-05-31
|
|
_
|
/
|
/
|
|
|
*
|
Reduce circular dependency constants <-> projections
Gaëtan Gilbert
2018-05-31
*
|
|
[api] Remove deprecated object from `Term`
Emilio Jesus Gallego Arias
2018-05-30
|
/
/
*
|
Merge PR #7558: [api] Make `vernac/` self-contained.
Maxime Dénès
2018-05-30
|
\
\
*
\
\
Merge PR #7621: Tactics.introduction: remove dangerous option ~check
Pierre-Marie Pédrot
2018-05-30
|
\
\
\
*
\
\
\
Merge PR #7521: Fix soundness bug with VM/native and cofixpoints
Pierre-Marie Pédrot
2018-05-28
|
\
\
\
\
|
|
*
|
|
Tactics.introduction: remove dangerous option ~check
Enrico Tassi
2018-05-28
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Unify pre_env and env
Maxime Dénès
2018-05-28
*
|
|
|
Merge PR #7419: Remove 100 occurrences of Evd.empty
Pierre-Marie Pédrot
2018-05-28
|
\
\
\
\
|
|
/
/
/
|
/
|
|
|
|
|
*
|
[api] Make `vernac/` self-contained.
Emilio Jesus Gallego Arias
2018-05-27
|
|
*
|
[tactics] Turn boolean locality hint parameter into a named one.
Emilio Jesus Gallego Arias
2018-05-27
|
|
/
/
|
/
|
|
*
|
|
Merge pull request #7569 from ppedrot/clean-newring
Assia Mahboubi
2018-05-25
|
\
\
\
*
\
\
\
Merge PR #7524: [ssr] fix after to_constr ~abort_on_undefined_evars was added
Maxime Dénès
2018-05-25
|
\
\
\
\
|
|
|
*
|
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-25
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
[tactics] Remove anonymous fix/cofix form.
Emilio Jesus Gallego Arias
2018-05-24
*
|
|
|
Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...
Pierre-Marie Pédrot
2018-05-24
|
\
\
\
\
|
*
|
|
|
Moving Option.smart_map to Option.Smart.map.
Hugo Herbelin
2018-05-23
|
*
|
|
|
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-23
|
*
|
|
|
Collecting Array.smart_* functions into a module Array.Smart.
Hugo Herbelin
2018-05-23
*
|
|
|
|
[api] Move `opacity_flag` to `Proof_global`.
Emilio Jesus Gallego Arias
2018-05-23
|
/
/
/
/
[next]