index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
glob_ops.ml
Commit message (
Expand
)
Author
Age
*
change into QuestionMark default
Siddharth Bhat
2018-07-17
*
Change QuestionMark for better record field missing error message.
Siddharth Bhat
2018-07-17
*
Glob_ops.rename_glob_vars: fix typo
Gaëtan Gilbert
2018-07-03
*
Glob_ops.fix_kind_eq: fix typo
Gaëtan Gilbert
2018-07-03
*
Remove reference name type.
Maxime Dénès
2018-06-18
*
Fixes #7811 (uncaught Not_found in notation printer related to "match").
Hugo Herbelin
2018-06-17
*
Merge PR #7105: Getting rid of some false "collision between bound variable n...
Matthieu Sozeau
2018-06-14
|
\
*
|
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-12
*
|
[api] Remove deprecated object from `Term`
Emilio Jesus Gallego Arias
2018-05-30
*
|
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] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-05-04
*
|
Glob_ops: cosmetic renaming to reflect the type of objects.
Hugo Herbelin
2018-03-28
|
*
Getting rid of some false "collision between bound variable names" warnings.
Hugo Herbelin
2018-03-28
|
/
*
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-09
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
Using an "as" clause when needed for printing irrefutable patterns.
Hugo Herbelin
2018-02-20
*
Adding patterns in the category of binders for notations.
Hugo Herbelin
2018-02-20
*
Canonically add an encoding in glob_constr of "as" operator for cases_pattern.
Hugo Herbelin
2018-02-20
*
Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.
Hugo Herbelin
2018-02-20
*
Use r.(p) syntax to print primitive projections.
Maxime Dénès
2018-01-30
*
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-13
*
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
2017-10-25
*
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-28
*
Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).
Hugo Herbelin
2017-09-23
*
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-09-04
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
A fix to #5414 (ident bound by ltac names now known for "match").
Hugo Herbelin
2017-06-09
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-06-08
|
\
*
\
Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...
Maxime Dénès
2017-06-05
|
\
\
*
\
\
Merge PR#561: Improving the Name API
Maxime Dénès
2017-06-01
|
\
\
\
|
|
*
|
Using a more explicit algebraic type for evars of kind "MatchingVar".
Hugo Herbelin
2017-05-31
|
*
|
|
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-31
|
|
/
/
*
/
/
Fixing #5523 (missing support for complex constructions in recursive notations).
Hugo Herbelin
2017-05-31
|
/
/
*
|
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
|
*
|
Remove dead code and unused open.
Maxime Dénès
2017-05-05
*
|
|
[location] [ast] Port module AST to CAst
Emilio Jesus Gallego Arias
2017-04-25
*
|
|
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
*
|
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
*
|
|
[location] Switch glob_constr to Loc.located
Emilio Jesus Gallego Arias
2017-04-24
*
|
|
[location] Move Glob_term.predicate_pattern to located.
Emilio Jesus Gallego Arias
2017-04-24
*
|
|
[location] Move Glob_term.cases_pattern to located.
Emilio Jesus Gallego Arias
2017-04-24
|
*
|
Using fold_glob_constr_with_binders to code bound_glob_vars.
Hugo Herbelin
2017-04-13
|
*
|
Adding a fold_glob_constr_with_binders combinator.
Hugo Herbelin
2017-04-13
|
/
/
|
*
Better support for printing constructors with let-ins.
Hugo Herbelin
2017-04-07
*
|
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
|
/
*
A new step on using alpha-conversion in printing notations.
Hugo Herbelin
2016-07-18
*
Partial fix to #4592 (notation requiring alpha-conversion for printing).
Hugo Herbelin
2016-07-17
*
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
[next]