| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-03 | Merge PR#411: Mention template polymorphism in the documentation. | Maxime Dénès | |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert | |
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert | |
| 2017-04-27 | Fix omitted labels in function calls | Gaetan Gilbert | |
| 2017-04-27 | Merge PR#586: trivial cleanup commits which does not change Coq API | Maxime Dénès | |
| 2017-04-27 | contracting the type of "Pfedit.solve_by_implicit_tactic" | Matej Košík | |
| 2017-04-24 | Removing the tclWEAK_PROGRESS tactical. | Pierre-Marie Pédrot | |
| The only remaining use was applied on the unfold tactic, and the behaviours of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced by their argument tactic. | |||
| 2017-04-24 | Removing the tclNOTSAMEGOAL primitive from the API. | Pierre-Marie Pédrot | |
| The only use in Equality is reimplemented in the new engine. | |||
| 2017-04-24 | Merge PR#552: Miscelaneous commits | Maxime Dénès | |
| 2017-04-21 | Remove VernacError | Gaetan Gilbert | |
| 2017-04-20 | COMMENT: Proof_global.pstate.pid | Matej Kosik | |
| 2017-04-11 | Update various comments to use "template polymorphism" | Gaetan Gilbert | |
| Also remove obvious comments. | |||
| 2017-04-07 | Merge branch 'master' into econstr | Pierre-Marie Pédrot | |
| 2017-04-06 | Merge PR#508: Optimize pending evars | Maxime Dénès | |
| 2017-04-04 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-04-01 | Using delayed universe instances in EConstr. | Pierre-Marie Pédrot | |
| The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. | |||
| 2017-03-29 | Fix call to broken unsafe_type_of in apply tactic. | Maxime Dénès | |
| This broke the build of iris-coq in the EConstr branch. Each time you use unsafe_type_of, I loose a night of sleep, so please stop. | |||
| 2017-03-24 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-03-24 | [nit] Fix a couple incorrect uses of msg_error. | Emilio Jesus Gallego Arias | |
| 2017-03-23 | Fast path for implicit tactic solving. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-03-21 | [pp] [ide] Minor cleanups in pp code. | Emilio Jesus Gallego Arias | |
| - 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. | |||
| 2017-03-13 | Remove a dead exception catching code. | Théo Zimmermann | |
| 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. | |||
| 2017-02-15 | [stm] Break stm/toplevel dependency loop. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-02-14 | Merge branch 'master'. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing most nf_enter in tactics. | Pierre-Marie Pédrot | |
| Now they are useless because all of the primitives are (should?) be evar-insensitive. | |||
| 2017-02-14 | Namegen primitives now apply on evar constrs. | Pierre-Marie Pédrot | |
| 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. | |||
| 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 | |
| This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization. | |||
| 2017-02-14 | Definining EConstr-based contexts. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-02-14 | Introducing contexts parameterized by the inner term type. | Pierre-Marie Pédrot | |
| This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms. | |||
| 2017-02-14 | Evar-normalizing functions now act on EConstrs. | 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 | 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 | 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 | Rewrite API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Eqdecide API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Hints API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tactics 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 | 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |