index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
detyping.ml
Commit message (
Expand
)
Author
Age
*
Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42...
Maxime Dénès
2017-10-03
|
\
*
|
Efficient computation of the names contained in an environment.
Pierre-Marie Pédrot
2017-09-28
*
|
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-28
|
*
After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.
Hugo Herbelin
2017-09-23
|
/
*
Proposing meta names more distinguishable from evar names than ?M42.
Hugo Herbelin
2017-09-21
*
A possible fix to BZ#5750 (ability to print context of ltac subterm match).
Hugo Herbelin
2017-09-21
*
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-09-04
*
Prevent overallocation in Array.map_to_list and remove custom implementation ...
Guillaume Melquiond
2017-08-22
*
Merge PR #913: Less allocations in Detyping
Maxime Dénès
2017-08-01
|
\
*
|
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
|
*
Add a comment regarding the specialization of the combinator in Detyping.
Pierre-Marie Pédrot
2017-07-26
|
*
Allocation-friendly detyping of term arrays.
Pierre-Marie Pédrot
2017-07-21
|
/
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
Don't double up on periods in anomalies
Jason Gross
2017-06-02
*
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-31
*
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-25
|
\
*
\
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
|
|
*
[option] Remove support for non-synchronous options.
Emilio Jesus Gallego Arias
2017-05-24
|
|
/
|
*
Merge PR#544: Anonymous universes
Maxime Dénès
2017-05-05
|
|
\
|
|
*
Allow flexible anonymous universes in instances and sorts.
Gaetan Gilbert
2017-05-03
|
*
|
applied the patch for printing types of let bindings by @herbelin
Abhishek Anand (@brixpro-home)
2017-05-02
|
|
/
|
*
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] 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
|
/
*
Merge PR#379: Introducing evar-insensitive constrs
Maxime Dénès
2017-04-11
|
\
*
|
Turning the printing primitive projection parameter flag off by default.
Hugo Herbelin
2017-04-07
*
|
Turning the printing primitive projection compatibility flag off by default.
Hugo Herbelin
2017-04-07
|
*
Merge branch 'trunk' into pr379
Maxime Dénès
2017-04-04
|
|
\
|
|
/
|
/
|
|
*
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-04-01
|
*
Actually exporting delayed universes in the EConstr implementation.
Pierre-Marie Pédrot
2017-04-01
*
|
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
|
*
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
|
*
Moving printing code from Evd to Termops.
Pierre-Marie Pédrot
2017-02-14
|
*
Removing compatibility layers in Retyping
Pierre-Marie Pédrot
2017-02-14
|
*
Removing some return type compatibility layers in Termops.
Pierre-Marie Pédrot
2017-02-14
|
*
Eliminating parts of the right-hand side compatibility layer
Pierre-Marie Pédrot
2017-02-14
|
*
Tactic_matching API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
*
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
*
Cleaning up opening of the EConstr module in pretyping folder.
Pierre-Marie Pédrot
2017-02-14
|
*
Retyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
*
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
*
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
/
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
*
Two protections against failures when printing evar_map.
Hugo Herbelin
2016-08-17
[next]