index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
cases.ml
Age
Commit message (
Expand
)
Author
2015-12-05
About building of substitutions from instances.
Hugo Herbelin
2015-10-18
Using appropriate lambda decomposition function counting let-ins when
Hugo Herbelin
2015-10-09
Fix inference of return clause raising a type error.
Matthieu Sozeau
2015-10-08
Univs: fix bug #4161.
Matthieu Sozeau
2015-09-08
Documenting the code when preference is given to expansion of default
Hugo Herbelin
2015-05-13
Safer typing primitives.
Pierre-Marie Pédrot
2015-02-27
Fixing first part of bug #3210 (inference of pattern-matching return
Hugo Herbelin
2015-02-10
Fixing #4001 (missing type constraints when building return clause of match).
Hugo Herbelin
2015-01-12
Update headers.
Maxime Dénès
2014-12-11
Tentatively more informative report of failure when inferring
Hugo Herbelin
2014-12-08
Fixing wrong evar_map in return clause inference, revealed by 48509b611.
Hugo Herbelin
2014-12-07
Improved tracking of the origin of evars.
Hugo Herbelin
2014-10-22
Fixing an evar leak in pattern-matching compilation (#3758).
Hugo Herbelin
2014-10-17
When facing problem ?id = ?id' in resolution of return predicate,
Hugo Herbelin
2014-10-15
Make use of unfolded primitive projections when elaborating match on a
Matthieu Sozeau
2014-10-13
Added support for several impossible cases in compilation of "match".
Hugo Herbelin
2014-10-11
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
Matthieu Sozeau
2014-10-05
A few improvements on pattern-matching compilation.
Hugo Herbelin
2014-10-04
A few Global.env removed.
Hugo Herbelin
2014-09-30
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-27
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-13
Providing a -type-in-type option for collapsing the universe hierarchy.
Hugo Herbelin
2014-09-12
An old typo which was preventing example #3537 to work the same as it
Hugo Herbelin
2014-09-12
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-06
Fix bug #3584, elaborating pattern-matching on primitive records to the
Matthieu Sozeau
2014-09-04
Typing.sort_of does not leak evarmaps anymore.
Pierre-Marie Pédrot
2014-08-01
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-06-26
Change interface of refresh universes to get a pbty argument instead of
Matthieu Sozeau
2014-06-24
Fix program cases and inversion tactic to correctly record universe constraints.
Matthieu Sozeau
2014-06-20
Cleanup treatment of template universe polymorphism (thanks to E. Tassi
Matthieu Sozeau
2014-06-04
Collecting in Namegen those conventional default names that are used in diffe...
Hugo Herbelin
2014-05-06
Refresh some universes in cases.ml as they might appear in the term.
Matthieu Sozeau
2014-05-06
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").
Yves Bertot
2014-05-06
Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
Matthieu Sozeau
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-04-23
Better representation of evar filters: we represent the vacuous filters of
Pierre-Marie Pédrot
2014-04-23
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-02-12
TC: honor the use_typeclasses flag in pretyping
Enrico Tassi
2013-12-06
Fix test-suite/success/evars.v.
Arnaud Spiwack
2013-11-27
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-02
Fix compilation of pattern matching wrt variables: alias.
aspiwack
2013-11-02
Fix the compilation of pattern matching wrt to variables.
aspiwack
2013-10-27
Abstracting evar filter away. The API is not perfect, but better than nothing.
ppedrot
2013-10-24
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
Turn many List.assoc into List.assoc_f
letouzey
2013-10-23
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-09-19
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-05-11
Fixing a source of evars leak, revealed by contrib QuicksortComplexity
herbelin
2013-05-09
Uniformization: isevars -> evdref/sigma/evd
herbelin
[next]
