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
*
Tacmach 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
*
Stronger static invariant in equality upto universes.
Pierre-Marie Pédrot
2016-10-31
*
Moving Universes to the engine/ folder.
Pierre-Marie Pédrot
2016-10-30
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
*
Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).
Hugo Herbelin
2016-10-29
|
*
Merge remote-tracking branch 'github/pr/337' into v8.6
Maxime Dénès
2016-10-28
|
|
\
|
|
*
Complete overhaul of the Arguments vernacular.
Maxime Dénès
2016-10-27
|
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-26
|
|
\
\
|
|
*
\
Merge remote-tracking branch 'github/pr/333' into v8.5
Maxime Dénès
2016-10-25
|
|
|
\
\
*
|
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-24
|
\
|
|
|
|
|
|
*
|
|
Remove incorrect assertion in cbn (bug #4822).
Guillaume Melquiond
2016-10-22
|
|
|
*
|
Fix a bug in error printing of unif constraints
Matthieu Sozeau
2016-10-22
|
|
|
/
/
|
*
|
|
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-10-21
|
|
\
|
|
|
|
*
|
Revert "unification.ml: fix for bug #4763, unif regression"
Maxime Dénès
2016-10-21
|
|
*
|
A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).
Hugo Herbelin
2016-10-20
|
*
|
|
Attempt to improve error rendering in pattern-matching compilation (#5142).
Hugo Herbelin
2016-10-19
*
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-18
|
\
|
|
|
|
*
|
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-18
|
|
\
|
|
|
*
|
|
Quick fix to unification regression #4955.
Hugo Herbelin
2016-10-17
|
|
|
/
|
|
/
|
|
|
*
Fixing to #3209 (Not_found due to an occur-check cycle).
Hugo Herbelin
2016-10-17
|
|
*
Fixing a missing constraint in consider_remaining_unif_constraints.
Hugo Herbelin
2016-10-17
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-17
|
\
|
|
|
*
|
Completing reverting generalization and cleaning of the return clause inference.
Hugo Herbelin
2016-10-13
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-12
|
\
|
|
|
*
|
Reverting generalization and cleaning of the return clause inference in v8.6.
Hugo Herbelin
2016-10-11
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-08
|
\
|
|
|
*
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-08
|
|
\
|
[next]
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
Guillaume Melquiond
Matthieu Sozeau
Matthieu Sozeau