Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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 |
| | | | | | | | | | This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules. | ||
* | 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 |
| |