aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
* Removing unused Refiner.tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
|
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
|
* Hypotheses in [Proofview.Goal.enter] were not normalised.Gravatar Arnaud Spiwack2014-08-07
| | | Fixes PTSF (though I have no idea what caused this bug to show up just yesterday).
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
| | | | | This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine. As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.
* Adding a [make] primitive to the NonLogical monad.Gravatar Pierre-Marie Pédrot2014-08-05
|
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
|
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
| | | | | | | | | | | | | obtained from case analysis or induction. Made it under experimental status. This replaces commit bf7d2a3ad2535e7d57db79c17c81aaf67d956965 which was acting at the level of logic.ml. Now acting in tactics.ml. Parts of things to be done about naming (not related to Propositions): induction on H:nat+bool produces hypotheses n and b but destruct on H produces a and b. This is because induction takes the dependent scheme whose names are statically inferred to be a and b while destruct dynamically builds a new scheme.
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
| | | | | par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
* Goal: API to get the solution of a goalGravatar Enrico Tassi2014-08-05
|
* Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Gravatar Arnaud Spiwack2014-08-05
| | | | | When "entering" in a goal, the environment observed by [tclENV] is changed (in the scope of the goal) to be that of the goal. I'm not entirely sure it is the right semantics. But it allows to write tactics which are agnostic of whether they are run in a goal or not.
* Some comments in the interface of Proofview_monad.Gravatar Arnaud Spiwack2014-08-04
|
* Cleaning the new implementation of the tactic monad continued.Gravatar Arnaud Spiwack2014-08-04
| | | | Remove proofview_gen, which was the repository of the extracted code, and move it to proofview_monad, which has the actual interface used by the [Proofview] module to implement tactics.
* Cleaning of the new implementation of the tactic monad.Gravatar Arnaud Spiwack2014-08-04
| | | | | | | | | * Add comments in the code (mostly imported from Monad.v) * Inline duplicated module * Clean up some artifacts due to the extracted code. * [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally) * Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code). * Remove Monad.v
* Add primtive [num_goal] to Proofview.Gravatar Arnaud Spiwack2014-08-01
| | | | The [num_goal] tactic counts the number of focused goals.
* Clean outdated comment in Proofview.Notations.Gravatar Arnaud Spiwack2014-08-01
|
* Removing more tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
|
* Making the error message about bullets more precise.Gravatar Pierre Courtieu2014-07-31
| | | | Suggests in some cases the right bullet to use.
* Adding a tclBREAK primitive to the tactic monad.Gravatar Pierre-Marie Pédrot2014-07-28
|
* Add a tactic [swap i j] to swap the position of goals [i] and [j].Gravatar Arnaud Spiwack2014-07-25
| | | If [i] or [j] is negative goals are counted from the end.
* Adds a cycle tactic to reorder goals in a loop.Gravatar Arnaud Spiwack2014-07-25
| | | [cycle 1] puts the first goal last, [cycle -1] puts the last goal first, [cycle n] is like [do n cycle 1], [cycle -n] is like [do n cycle -1].
* Small reorganisation in proof.ml.Gravatar Arnaud Spiwack2014-07-25
|
* Fail gracefully when focusing on non-existing goals with user commands.Gravatar Arnaud Spiwack2014-07-25
| | | Fixes bug #3457
* Fix handling of universes at the end of proofs, esp. for async proof processing.Gravatar Matthieu Sozeau2014-07-25
| | | | Thanks to E. Tassi for the initial patch.
* A handful of useful primitives in Proofview.Refine.Gravatar Arnaud Spiwack2014-07-24
|
* Adding a tail-rec tclONCE.Gravatar Pierre-Marie Pédrot2014-07-24
|
* New implementation of the tactic monad.Gravatar Pierre-Marie Pédrot2014-07-24
| | | | | | | | | The new implementation is made of two layers: a iolist, which is essentially a stream without memoization, and above this a state monad. The previous design of the extracted monad kept three distinct but similar monad transformers: a stateT, a writerT and a readerT. We take advantage of this similarity to pack those three transformers into only one state monad. This makes the code cleaner and hopefully more efficient.
* When closing a proof, make sure that the types have their evar substituted.Gravatar Arnaud Spiwack2014-07-23
| | | | When starting proofs with [start_dependent_proof], we may have initial goals with existential variables in their conclusion. They will be solved by the proof, but this information was not propagated in close proof, and the kernel failed on uninstanciated evars.
* Proof_global: an unused variable replaced by a wildcard.Gravatar Arnaud Spiwack2014-07-23
|
* Proof_global.start_dependent_proof: properly threads the sigma through the ↵Gravatar Arnaud Spiwack2014-07-23
| | | | | telescope. Allows for a more refined notion of dependently generated initial goals.
* Change the interface of proof_global to take an evar_map instead of a ↵Gravatar Arnaud Spiwack2014-07-23
| | | | | universe context to start proofs. It was kind of awkward to work with for non-traditionnal kinds of proofs: if you have an evar_universe_context, you got it from a sigma anyway.
* Adding a delay to tclTIME.Gravatar Pierre-Marie Pédrot2014-07-14
|
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
| | | | backtracks, print time spent in each of successive calls.
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
| | | | | LoadedFile is generated when a .vo is loaded Goals is generated when -feedback-goals
* check_for_interrupt: better (but slower) in threading modeGravatar Enrico Tassi2014-07-10
| | | | | Experimenting with PIDE I discovered that yield is not sufficient to have a rescheduling, hence the delay.
* Exporting Proof.split in proofview.Gravatar Pierre-Marie Pédrot2014-07-08
|
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
| | | | This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.
* time tacGravatar Hugo Herbelin2014-07-07
|
* Putting implicit arguments of Clenv.res_pf right.Gravatar Pierre-Marie Pédrot2014-06-25
|
* Force the final universe context of a proof only in poly || now case.Gravatar Matthieu Sozeau2014-06-24
|
* Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itGravatar Pierre-Marie Pédrot2014-06-24
| | | | | exhibits the "useless goal" behaviour: there is code out there depending on the fact that goals cannot be solved by side effects.
* Clenvtac.res_pf is in the new tactic monad.Gravatar Pierre-Marie Pédrot2014-06-24
|
* Clenvtac.unify is in the new monad.Gravatar Pierre-Marie Pédrot2014-06-23
|
* Adding a raw_goals primitive for Tacinterp.Gravatar Pierre-Marie Pédrot2014-06-19
|
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
| | | | | | and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup.
* Tentative optimization not to nf_evar too often in the compatibilityGravatar Pierre-Marie Pédrot2014-06-17
| | | | | | layer. To this intent, we add a cache evar_map in goals that is the latest known one where the goal is nf-evarized. If the current one and the cache coincide, we leave the goal as-is.
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
|
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
| | | | | | | a projection constant only of the form λ params (r : I params), match r with BuildR args => args_i end, without any other user input and relies on it being typable (no more primitive projections escaping this).
* Improving tclWITHHOLES which did not see undefined evars up toGravatar Hugo Herbelin2014-06-13
| | | | | restriction, after last fix commit which precisely possibly restricts evars of a term "t" in "apply t in H" without resolving them.
* Fixing "clear" in internal_cut_replace: forbid dependencies in theGravatar Hugo Herbelin2014-06-13
| | | | name of replaced hypothesis.
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in ↵Gravatar Matthieu Sozeau2014-06-10
| | | | | | | | Universes. Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes. Remove unused functions from univ as well and refactor a little bit. Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 17:51:56 +0000