index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
notation_ops.ml
Age
Commit message (
Expand
)
Author
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
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
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
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-01-30
Use r.(p) syntax to print primitive projections.
Maxime Dénès
2017-11-23
Make some functions on terms more robust w.r.t new term constructs.
Maxime Dénès
2017-11-13
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-09-28
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-12
Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.
Hugo Herbelin
2017-09-12
Fixing a typo in printing notations with recursive binders.
Hugo Herbelin
2017-09-12
Fixing a bug of recursive notations introduced in dfdaf4de.
Hugo Herbelin
2017-09-04
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-08-29
Adapting code to renaming Array.fold_map -> Array.fold_left_map.
Hugo Herbelin
2017-08-29
Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map
Hugo Herbelin
2017-07-04
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-15
Merge PR#713: Bump year in headers.
Maxime Dénès
2017-06-09
Fix Bug #5568, no dup notation warnings on repeated module imports
Paul Steckler
2017-06-08
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-01
Merge PR#561: Improving the Name API
Maxime Dénès
2017-06-01
Bump year in headers.
Maxime Dénès
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
Fixing a too lax constraint for finding recursive binder part of a notation.
Hugo Herbelin
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-04-27
Remove some unused values and types
Gaetan Gilbert
2017-04-25
[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-24
[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-07
Better support for printing constructors with let-ins.
Hugo Herbelin
2017-04-04
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
Using the same type of binders for interning and externing.
Hugo Herbelin
2017-02-14
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2016-10-29
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-27
Fixing #5161 (case of a notation with unability to detect a recursive binder).
Hugo Herbelin
[prev]
[next]
