aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
* Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\
* \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \
| | * | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
| * | | Merge PR#642: Small cleanup on `close_proof` type.Gravatar Maxime Dénès2017-05-24
| |\ \ \ | | |/ / | |/| |
| | * | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc...
| * | | Change wrong bullet message.Gravatar Théo Zimmermann2017-05-20
| |/ / | | | | | | | | | | | | | | | Remove a space before colon. Remove the use of term mandatory (this closes https://coq.inria.fr/bugs/show_bug.cgi?id=3994).
| | * Removing unused warnings.Gravatar Pierre-Marie Pédrot2017-05-19
| | |
| | * Generalizing the refine primitive so as to accept tactic arguments.Gravatar Pierre-Marie Pédrot2017-05-03
| |/
| * Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
| |\
| * | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | |
| * | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Merge PR#586: trivial cleanup commits which does not change Coq APIGravatar Maxime Dénès2017-04-27
| |\ \
| | * | contracting the type of "Pfedit.solve_by_implicit_tactic"Gravatar Matej Košík2017-04-27
| | | |
* | | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* | | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | Now it is a private field, locations are optional.
* | | | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
| |/ / |/| |
| * | Removing the tclWEAK_PROGRESS tactical.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | | | | | | | | | | | | | 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.
| * | Removing the tclNOTSAMEGOAL primitive from the API.Gravatar Pierre-Marie Pédrot2017-04-24
|/ / | | | | | | The only use in Equality is reimplemented in the new engine.
* | Merge PR#552: Miscelaneous commitsGravatar Maxime Dénès2017-04-24
|\ \
* | | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| | |
| * | COMMENT: Proof_global.pstate.pidGravatar Matej Kosik2017-04-20
|/ /
| * Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
|/ | | | Also remove obvious comments.
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
| * Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
| |\
* | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\| |
* | | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | | | | | | | | | | | | | 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.
* | | Fix call to broken unsafe_type_of in apply tactic.Gravatar Maxime Dénès2017-03-29
| | | | | | | | | | | | | | | 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.
* | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\ \ \
| | * | [nit] Fix a couple incorrect uses of msg_error.Gravatar Emilio Jesus Gallego Arias2017-03-24
| |/ /
| | * 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
| |