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
*
Completing reverting generalization and cleaning of the return clause inference.
Hugo Herbelin
2016-10-13
*
Reverting generalization and cleaning of the return clause inference in v8.6.
Hugo Herbelin
2016-10-11
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-08
|
\
*
|
Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq.
Pierre-Marie Pédrot
2016-10-08
*
|
Fix bug #4464: "Anomaly: variable H' unbound. Please report.".
Pierre-Marie Pédrot
2016-10-07
|
*
evarconv.ml: Fix bug #4529, primproj unfolding
Matthieu Sozeau
2016-10-06
|
*
w_merge: Add a comment about the (List.rev evars)
Matthieu Sozeau
2016-10-06
|
*
unification.ml: fix for bug #4763, unif regression
Matthieu Sozeau
2016-10-06
*
|
Quick fix to #4595 (making notations containing "ltac:" unused for printing).
Hugo Herbelin
2016-10-04
*
|
Merge remote-tracking branch 'github/pr/263' into v8.6
Maxime Dénès
2016-10-03
|
\
\
*
|
|
Fix bug #4723 and FIXME in API for solve_by_tac
Matthieu Sozeau
2016-09-28
*
|
|
Remove incorrect assertion in cbn (bug #4822).
Guillaume Melquiond
2016-09-28
*
|
|
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.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
*
|
|
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
*
|
|
|
Monomorphize a costly boolean equality operation.
Pierre-Marie Pédrot
2016-09-09
|
/
/
/
|
|
*
Tracking careless uses of slow name lookup.
Pierre-Marie Pédrot
2016-09-09
|
|
/
|
/
|
*
|
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
|
*
|
[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
|
\
\
*
|
|
Fix reopened bug #3317.
Matthieu Sozeau
2016-07-06
*
|
|
Disallow dependent case on prim records w/o eta
Matthieu Sozeau
2016-07-06
*
|
|
Renaming to more generic has_dependent_elim test
Matthieu Sozeau
2016-07-06
*
|
|
Move is_prim... to Inductiveops and correct Scheme
Matthieu Sozeau
2016-07-06
|
*
|
Univs: fix internalization of (x := T) and casts
Matthieu Sozeau
2016-07-06
|
/
/
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2016-07-04
|
\
\
|
|
*
congruence: Restrict refreshing to Set
Matthieu Sozeau
2016-07-04
[next]