aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
...
| | * | Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
| |/ / | | | | | | | | | | | | | | | We make apparent in the API that the implicit tactic is set or not. This was costing a lot in Pretyping for no useful reason, as it is almost always unset and the default implementation was just failing immediately.
| * | [pp] [ide] Minor cleanups in pp code.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | - We avoid unnecessary use of Pp -> string conversion functions. and the creation of intermediate buffers on logging. - We rename local functions that share the name with the Coq stdlib, this is usually dangerous as if the normal function is removed, code may pick up the one in the stdlib, with different semantics.
| * | Remove a dead exception catching code.Gravatar Théo Zimmermann2017-03-13
| | | | | | | | | | | | | | | | | | | | | The code was assuming that Proofview.tclFOCUS could raise a CList.IndexOutOfRange exception but this isn't the case. The focusing functions already catch this exception and raises an algebraic exception within the tactic mechanism.
| * | [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.
* | | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\| |
* | | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | Now they are useless because all of the primitives are (should?) be evar-insensitive.
* | | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough.
* | | Moving printing code from Evd to Termops.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Chasing a few unsafe constr coercions.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization.
* | | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
* | | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms.
* | | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Funind API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Quote API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Eqdecide API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Tacticals API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-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.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Nativenorm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Vnorm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
| * | Adding a printer for Proof.proof reflecting the focusing layout.Gravatar Hugo Herbelin2017-01-26
| | | | | | | | | | | | | | | | | | | | | | | | This is a modest contribution serving before all the purpose of displaying the focus stack and the shelf and give_up list. It does not print the sigma (while it could). Any improvements are welcome.
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
| |\|
| | * Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
| | | | | | | | | | | | | | | Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/| | | |/
| * Use pf_get_type_of to avoid blowup in pose proof of large proof termsGravatar Matthieu Sozeau2016-11-08
| |
| * Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ | | | | | | | | | Was PR#331: Solve_constraints and Set Use Unification Heuristics
| | * More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 23:22:15 +0000