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
*
Dedicated datatype for aliases in Evarsolve.
Pierre-Marie Pédrot
2017-02-14
*
Removing a subtle nf_enter in Class_tactics.
Pierre-Marie Pédrot
2017-02-14
*
Removing most nf_enter in tactics.
Pierre-Marie Pédrot
2017-02-14
*
Fix a mishandled exception in Omega.
Pierre-Marie Pédrot
2017-02-14
*
Putting back the occur_meta_or_undefined_evar function in the old term API.
Pierre-Marie Pédrot
2017-02-14
*
Moving evar-normalization functions to EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
*
Making Evd independent from Namegen.
Pierre-Marie Pédrot
2017-02-14
*
Moving printing code from Evd to Termops.
Pierre-Marie Pédrot
2017-02-14
*
Chasing a few unsafe constr coercions.
Pierre-Marie Pédrot
2017-02-14
*
Do not ask for a normalized goal to get hypotheses and conclusions.
Pierre-Marie Pédrot
2017-02-14
*
Putting back the subst_defined_metas_evars function in the old term API.
Pierre-Marie Pédrot
2017-02-14
*
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
*
Introducing contexts parameterized by the inner term type.
Pierre-Marie Pédrot
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
[next]