index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Refine API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Goal 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
*
Making judgment type generic over the type of inner constrs.
Pierre-Marie Pédrot
2017-02-14
*
Unification API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Pretyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Cases API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Coercion API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Classops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Typeclasses API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Tacred API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Constr_matching API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Patternops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Typing API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Evarconv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Recordops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Evarsolve API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Evardefine API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Find_subterm API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Cbv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Retyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Nativenorm API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Vnorm API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Introducing a new EConstr.t type to perform the nf_evar operation on demand.
Pierre-Marie Pédrot
2016-11-08
*
Revert "Better Arguments compatibility."
Maxime Dénès
2016-11-03
*
Merge branch 'v8.6' into trunk
Maxime Dénès
2016-11-03
|
\
|
*
Merge remote-tracking branch 'github/pr/341' into v8.6
Maxime Dénès
2016-11-03
|
|
\
*
|
|
updating ".merlin" file
Matej Kosik
2016-11-03
|
|
*
Better Arguments compatibility.
Maxime Dénès
2016-11-02
|
|
/
*
|
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
|
*
Fix spurious OCaml Warning 56 in TACTIC EXTEND macros.
Pierre-Marie Pédrot
2016-10-30
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
|
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-29
|
|
\
|
*
|
Removing dead code.
Hugo Herbelin
2016-10-29
|
*
|
Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).
Hugo Herbelin
2016-10-29
|
*
|
Fixing #5164 (regression in locating error in argument of "refine").
Hugo Herbelin
2016-10-29
|
*
|
Merge remote-tracking branch 'github/pr/321' into v8.6
Maxime Dénès
2016-10-28
|
|
\
\
|
*
\
\
Merge remote-tracking branch 'github/pr/319' into v8.6
Maxime Dénès
2016-10-28
|
|
\
\
\
|
*
\
\
\
Merge commit 'fccbd64' into v8.6
Maxime Dénès
2016-10-28
|
|
\
\
\
\
|
|
*
|
|
|
[build] Add a target to install the META file.
Emilio Jesus Gallego Arias
2016-10-28
|
|
*
|
|
|
[build] META file to enable plugin linking with ocamlfind.
Emilio Jesus Gallego Arias
2016-10-28
|
*
|
|
|
|
Merge remote-tracking branch 'github/pr/337' into v8.6
Maxime Dénès
2016-10-28
|
|
\
\
\
\
\
|
|
|
|
|
|
*
Fixing #5161 (case of a notation with unability to detect a recursive binder).
Hugo Herbelin
2016-10-27
*
|
|
|
|
|
|
COMMENT: unfortunatelly, ocamldoc does not recognize this kind of markup: it ...
Matej Kosik
2016-10-27
[prev]
[next]
Pierre-Marie Pédrot
Maxime Dénès
Matej Kosik
Hugo Herbelin
Emilio Jesus Gallego Arias