| Age | Commit message (Expand) | Author |
|---|---|---|
| 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 |
| 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 |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |