index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-27
|
\
|
*
Posssible abstractions over goal variables when inferring match return clause.
Hugo Herbelin
2016-09-26
|
*
Trying an abstracting dependencies heuristic for the match return clause even...
Hugo Herbelin
2016-09-26
|
*
Trying a no-inversion no-dependency heuristic for match return clause.
Hugo Herbelin
2016-09-26
|
*
Inference of return clause: giving uniformly priority to "small inversion".
Hugo Herbelin
2016-09-26
|
*
Fix bug #5096: [vm_compute] is exponentially slower than [native_compute].
Pierre-Marie Pédrot
2016-09-23
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-23
|
\
|
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-23
|
|
\
|
|
*
Fixing #5095 (non relevant too strict test in let-in abstraction).
Hugo Herbelin
2016-09-22
*
|
|
Make the Coq codebase independent from Ltac-related code.
Pierre-Marie Pédrot
2016-09-16
|
\
\
\
|
*
|
|
Untangling Tacexpr from lower strata.
Pierre-Marie Pédrot
2016-09-15
*
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-14
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
|
*
|
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-14
|
|
\
\
\
|
|
|
|
/
|
|
|
/
|
|
*
|
|
Merge remote-tracking branch 'github-coq/pr/249' into v8.6
Matthieu Sozeau
2016-09-12
|
|
\
\
\
|
|
|
*
|
Fixing #5077 (failure on typing a fixpoint with evars in its type).
Hugo Herbelin
2016-09-10
|
|
*
|
|
no-refold patch
Paul Steckler
2016-09-09
|
*
|
|
|
Fast path in Clenvtac.clenv_refine typeclass resolution.
Pierre-Marie Pédrot
2016-09-09
*
|
|
|
|
Propagate location info on pattern match compilation.
Emilio Jesus Gallego Arias
2016-09-09
|
*
|
|
|
Monomorphize a costly boolean equality operation.
Pierre-Marie Pédrot
2016-09-09
|
|
/
/
/
|
|
|
*
Unplugging Tacexpr in several interface files.
Pierre-Marie Pédrot
2016-09-08
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
\
\
*
|
|
|
CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...
Matej Kosik
2016-08-30
*
|
|
|
CLEANUP: using |> operator more consistently
Matej Kosik
2016-08-30
*
|
|
|
CLEANUP: taking advantage of "_ % _" operator to express function composition...
Matej Kosik
2016-08-29
*
|
|
|
CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...
Matej Kosik
2016-08-26
*
|
|
|
Merge remote-tracking branch 'v8.6' into trunk
Matej Kosik
2016-08-25
|
\
\
\
\
|
|
|
/
/
|
|
/
|
|
*
|
|
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
*
|
|
|
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
Matej Kosik
2016-08-24
*
|
|
|
CLEANUP: removing superfluous (module) qualifiers
Matej Kosik
2016-08-24
*
|
|
|
Changing the definition of the "Lib.variable.info" type to enable us to do mo...
Matej Kosik
2016-08-24
|
*
|
|
Merge PR #258: "Fix newline issues" into v8.6
Pierre-Marie Pédrot
2016-08-24
|
|
\
\
\
|
*
|
|
|
Pushing error backtrace in unification reraise.
Pierre-Marie Pédrot
2016-08-22
|
*
|
|
|
Do not recompute the whole evar naming environment in GProd intepretation.
Pierre-Marie Pédrot
2016-08-21
|
*
|
|
|
Short path for Pretyping.ltac_interp_name_env.
Pierre-Marie Pédrot
2016-08-21
|
/
/
/
/
*
|
|
|
Fixing a bug in the presence of let-in while inferring the return clause.
Hugo Herbelin
2016-08-20
|
|
*
|
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
|
*
|
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
|
*
|
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
|
|
/
/
|
/
|
|
|
*
|
[pp] Fix newline issues.
Emilio Jesus Gallego Arias
2016-08-19
|
/
/
*
|
Two protections against failures when printing evar_map.
Hugo Herbelin
2016-08-17
*
|
Efficiently generate the pretyping contexts.
Pierre-Marie Pédrot
2016-08-16
|
\
\
*
|
|
Make it a bit more obvious when variables are of type unit.
Guillaume Melquiond
2016-08-10
|
*
|
Using a dedicated kind of substitutions in evar name generation.
Pierre-Marie Pédrot
2016-08-06
|
*
|
Using the extended contexts in pretyping.
Pierre-Marie Pédrot
2016-08-05
|
*
|
Embedding the pretyping environment in a dummy record.
Pierre-Marie Pédrot
2016-08-04
|
/
/
*
|
A new step on using alpha-conversion in printing notations.
Hugo Herbelin
2016-07-18
*
|
Partial fix to #4592 (notation requiring alpha-conversion for printing).
Hugo Herbelin
2016-07-17
*
|
Remove spurious warnings about projections when requiring modules.
Pierre-Marie Pédrot
2016-07-08
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-07
|
\
|
*
|
Merge remote-tracking branch 'github/bug4653' into v8.6
Matthieu Sozeau
2016-07-07
|
\
\
[next]