| Age | Commit message (Collapse) | 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 | 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 | 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 | |
| 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. | |||
| 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 | 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 | Evarsolve API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Find_subterm API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Retyping 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 | |
| 2016-10-29 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-28 | Merge remote-tracking branch 'github/pr/321' into v8.6 | Maxime Dénès | |
| Was PR#321: Handling of section variables in hints | |||
| 2016-10-26 | Using msg_info for info_auto and info_eauto (PR #324). | Hugo Herbelin | |
| 2016-10-26 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-25 | Merge remote-tracking branch 'github/pr/338' into v8.5 | Maxime Dénès | |
| Was PR#338: Remove warning now that info_auto is fixed. | |||
| 2016-10-25 | Remove warning now that info_auto is fixed. | Théo Zimmermann | |
| Removes a warning dating from 8.5 signaling that info_auto and info_trivial are broken and advising to use Info 1 auto instead. Now, these tactics are fixed and thus they can be used again. They do not do exactly the same thing as Info 1 auto and may be more useful for the learner. | |||
| 2016-10-25 | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)." | Maxime Dénès | |
| This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6. This behavior of refine has changed three times in recent years, so let's take the time to make up our mind and wait for a major release. Btw, onhyps=None is not a sane way to express that a tactic should be applied to all hypotheses. | |||
| 2016-10-22 | Fixing printing of generic arguments of tag "var". | Hugo Herbelin | |
| 2016-10-21 | sections/hints: prevent Not_found in get_type_of | Matthieu Sozeau | |
| due to cleared/reverted section variables. This fixes the get_type_of but requires keeping information around about the section hyps available in goals during resolution. It's optimized for the non-section case (should incur no cost there), and the case where no section variables are cleared. | |||
| 2016-10-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |