index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
detyping.ml
Age
Commit message (
Expand
)
Author
2017-12-12
Decompiling pattern-matching: mini-removal dead code.
Hugo Herbelin
2017-12-12
In printing, factorizing "match" clauses with same right-hand side.
Hugo Herbelin
2017-12-01
Proper nametab handling of global universe names
Matthieu Sozeau
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-10-25
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
2017-10-03
Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42...
Maxime Dénès
2017-09-28
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-23
After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.
Hugo Herbelin
2017-09-21
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-04
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-08-22
Prevent overallocation in Array.map_to_list and remove custom implementation ...
Guillaume Melquiond
2017-08-01
Merge PR #913: Less allocations in Detyping
Maxime Dénès
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-26
Add a comment regarding the specialization of the combinator in Detyping.
Pierre-Marie Pédrot
2017-07-21
Allocation-friendly detyping of term arrays.
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
Don't double up on periods in anomalies
Jason Gross
2017-05-31
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-25
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-24
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-05
Merge PR#544: Anonymous universes
Maxime Dénès
2017-05-03
Allow flexible anonymous universes in instances and sorts.
Gaetan Gilbert
2017-05-02
applied the patch for printing types of let bindings by @herbelin
Abhishek Anand (@brixpro-home)
2017-04-27
Remove unused [open] statements
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-11
Merge PR#379: Introducing evar-insensitive constrs
Maxime Dénès
2017-04-07
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-04
Merge branch 'trunk' into pr379
Maxime Dénès
2017-04-01
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-03-24
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-02-14
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
[next]
