index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
patternops.ml
Commit message (
Expand
)
Author
Age
*
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-12
*
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-25
*
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
*
Evar maps contain econstrs.
Gaëtan Gilbert
2018-04-13
*
Supporting fix/cofix in Ltac pattern-matching (wish #7092).
Hugo Herbelin
2018-03-28
*
Patterns: Accepting patterns in PFix and PCofix and not only constr.
Hugo Herbelin
2018-03-28
*
Patternops: renaming an internal function to more closely match its effect.
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
*
Use r.(p) syntax to print primitive projections.
Maxime Dénès
2018-01-30
*
Make some functions on terms more robust w.r.t new term constructs.
Maxime Dénès
2017-11-23
*
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-13
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
Fixing #5401 (printing of patterns with bound anonymous variables).
Hugo Herbelin
2017-10-28
*
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-09-04
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-06-08
|
\
*
\
Merge PR#716: Don't double up on periods in anomalies
Maxime Dénès
2017-06-06
|
\
\
*
\
\
Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...
Maxime Dénès
2017-06-05
|
\
\
\
|
|
*
|
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
|
|
/
/
|
/
|
|
|
*
|
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
|
/
/
*
|
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
|
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
|
*
|
Fixing an extra bug with pattern_of_constr.
Hugo Herbelin
2017-05-19
|
|
*
fix swapping of ids in tuples, bug 5486
Paul Steckler
2017-05-17
|
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-05-17
|
|
\
|
|
|
*
Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
Hugo Herbelin
2017-05-01
|
|
*
Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."
Maxime Dénès
2017-04-28
|
|
*
Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
Hugo Herbelin
2017-04-28
|
*
|
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
*
|
|
[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] 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
|
/
/
*
|
Fix bug #5476: Ltac has an inconsistent view of hypotheses.
Pierre-Marie Pédrot
2017-04-19
*
|
Silence a few OCaml warnings.
Guillaume Melquiond
2017-04-13
*
|
Merge branch 'trunk' into pr379
Maxime Dénès
2017-04-04
|
\
\
*
|
|
Fix interpretation of Ltac patterns episode 2.
Maxime Dénès
2017-03-24
*
|
|
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
|
|
/
/
|
*
|
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-03-23
|
|
\
|
|
|
*
Intern names bound in match patterns
Tej Chajed
2017-03-23
*
|
|
Quick hack to fix interpretation of patterns in Ltac.
Pierre-Marie Pédrot
2017-02-14
*
|
|
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
[next]