index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2017-02-14
Evar-normalizing functions now act on EConstrs.
Pierre-Marie Pédrot
2017-02-14
Removing compatibility layers from Tacticals
Pierre-Marie Pédrot
2017-02-14
Cleaning up interfaces.
Pierre-Marie Pédrot
2017-02-14
Omega API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Micromega API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Removing various compatibility layers of tactics.
Pierre-Marie Pédrot
2017-02-14
Funind API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Removing compatibility layers related to printing.
Pierre-Marie Pédrot
2017-02-14
Ltac now uses evar-based constrs.
Pierre-Marie Pédrot
2017-02-14
Removing compatibility layers in Retyping
Pierre-Marie Pédrot
2017-02-14
Removing some return type compatibility layers in Termops.
Pierre-Marie Pédrot
2017-02-14
Setoid_ring API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Cc API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Quote API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Reductionops now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
Proofview.Goal primitive now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
Eliminating parts of the right-hand side compatibility layer
Pierre-Marie Pédrot
2017-02-14
Tauto API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Rewrite API using EConstr.
Pierre-Marie Pédrot
2017-02-14
G_class API using Econstr.
Pierre-Marie Pédrot
2017-02-14
G_auto API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Extratactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Tactic_matching API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Eqdecide API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Class_tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Eauto API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Auto API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Hints API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Leminv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Inv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Contradiction API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Equality API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Elim API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Hipattern API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Tacticals API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Clenv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Tacmach API using EConstr.
Pierre-Marie Pédrot
2017-02-14
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
[next]