index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
engine
Commit message (
Expand
)
Author
Age
*
Ensuring static invariants about handling of pending evars in Pretyping.
Pierre-Marie Pédrot
2017-03-23
*
[pp] Remove uses of expensive string_of_ppcmds.
Emilio Jesus Gallego Arias
2017-03-21
*
Proofview: tclINDEPENDENTL
Enrico Tassi
2017-02-10
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-02-01
|
\
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2017-01-23
*
|
Adding a new evar source to remember the name of evars which were
Hugo Herbelin
2017-01-22
*
|
Merge remote-tracking branch 'github/pr/350' into trunk
Maxime Dénès
2017-01-09
|
\
\
*
\
\
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-12-07
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Document changes
Matthieu Sozeau
2016-12-02
|
*
|
Fix UGraph.check_eq!
Matthieu Sozeau
2016-11-30
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-18
|
\
|
|
|
|
*
tclDISPATCH: more informative error message
Arnaud Spiwack
2016-11-08
|
|
/
|
/
|
|
*
Merge remote-tracking branch 'github/pr/339' into v8.6
Maxime Dénès
2016-11-07
|
|
\
|
|
*
Fixes to compile with ocaml 4.01
Matthieu Sozeau
2016-11-07
|
*
|
Merge commit 'e6edb33' into v8.6
Maxime Dénès
2016-11-07
|
|
\
\
|
|
|
/
|
|
/
|
*
|
|
Moving unused code out of the kernel into Termops.
Pierre-Marie Pédrot
2016-10-31
*
|
|
Stronger static invariant in equality upto universes.
Pierre-Marie Pédrot
2016-10-31
*
|
|
Code factorization in Universes.
Pierre-Marie Pédrot
2016-10-31
*
|
|
Moving Universes to the engine/ folder.
Pierre-Marie Pédrot
2016-10-30
*
|
|
Reordering Termops w.r.t. Evd and Namegen in engine folder.
Pierre-Marie Pédrot
2016-10-30
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
|
|
*
|
Merge remote-tracking branch 'github/pr/321' into v8.6
Maxime Dénès
2016-10-28
|
|
\
\
|
*
|
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-26
*
|
|
|
COMMENT: Namegen.next_ident_away
Matej Kosik
2016-10-26
*
|
|
|
COMMENT: Proofview.entry
Matej Kosik
2016-10-26
*
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-24
|
\
|
|
|
|
|
|
*
Unification constraint handling (#4763, #5149)
Matthieu Sozeau
2016-10-22
|
|
|
/
|
|
/
|
|
*
|
Oops, my bad, didn't expect a merge issue!
Matthieu Sozeau
2016-10-21
|
*
|
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-10-21
|
|
*
sections/hints: prevent Not_found in get_type_of
Matthieu Sozeau
2016-10-21
|
|
/
*
|
CLEANUP: Namegen.to_avoid
Matej Kosik
2016-10-20
*
|
CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".
Matej Kosik
2016-10-19
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-17
|
\
|
|
*
Fix bug #5145: Anomaly: index to an anonymous variable.
Pierre-Marie Pédrot
2016-10-15
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-12
|
\
|
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-12
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-12
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-05
|
\
|
|
*
Merge remote-tracking branch 'github/pr/263' into v8.6
Maxime Dénès
2016-10-03
|
|
\
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-23
|
\
|
|
|
*
|
Adding variants enter_one and refine_one which assume that exactly one
Hugo Herbelin
2016-09-16
|
|
*
Tracking careless uses of slow name lookup.
Pierre-Marie Pédrot
2016-09-09
|
|
/
*
|
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
\
*
\
\
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-07
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Fast path in push_rel_context_to_named_context.
Pierre-Marie Pédrot
2016-09-05
|
*
|
Fast path in whd_evar.
Pierre-Marie Pédrot
2016-09-02
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-02
|
\
|
|
|
*
|
Short documentation, filling TODO's in evd.mli.
Hugo Herbelin
2016-09-01
*
|
|
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
[next]