aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
* Fixing strange evarmap leak in goals.Gravatar Pierre-Marie Pédrot2014-09-18
| | | | | | Goals have to be refreshed when observed, because the evarmap may have changed between the moment where the goal was generated and the moment the goal is used.
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
|
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
| | | | equality of universes, along with a few other functions in evd.
* Revert "While resolving typeclass evars in clenv, touch only the ones that ↵Gravatar Matthieu Sozeau2014-09-17
| | | | | | | | appear in the" This reverts commit 9de1edd730eeb3cada742a27a36bc70178eda6d8. Not the right way to do it. The evd shouldn't contain unrelated evars in the first place.
* While resolving typeclass evars in clenv, touch only the ones that appear in theGravatar Matthieu Sozeau2014-09-17
| | | | | clenv's value and type, ensuring we don't try to solve unrelated goals (fixes bug#3633).
* Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Gravatar Arnaud Spiwack2014-09-15
| | | | All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).
* While we don't have a clean alternative to Clenvtac, add a primitiveGravatar Matthieu Sozeau2014-09-12
| | | | for tclEVARS which might solve existing goals.
* Add syntax [id]: to apply tactic to goal named id.Gravatar Hugo Herbelin2014-09-12
|
* Use evar name to print goal.Gravatar Hugo Herbelin2014-09-12
|
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
|
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
| | | | | instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
* No plural for only one non existing focused goal.Gravatar Hugo Herbelin2014-09-12
|
* Fix source of initial goal.Gravatar Hugo Herbelin2014-09-12
|
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
| | | | | | | | | | selection (rewrite, destruct/induction, set or apply on scheme), for unification (apply on not a scheme, auto), the latter being separated into primary unification and unification for merging instances. No change of semantics from within Coq, if I did not mistake (but a function like secondOrderAbstraction does not set flags by itself anymore).
* Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Gravatar Hugo Herbelin2014-09-10
|
* Display number of available goals in "incorrect number of goals" error message.Gravatar Arnaud Spiwack2014-09-08
|
* Add a tactic [revgoals] to reverse the list of focused goals.Gravatar Arnaud Spiwack2014-09-08
|
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
| | | | | | | | | | | 1. Proofview.Goal.enter into Proofview.Goal.nf_enter. 2. Proofview.Goal.raw_enter into Proofview.Goal.enter. 3. Proofview.Goal.goals -> Proofview.Goals.nf_goals 4. Proofview.Goal.raw_goals -> Proofview.Goals.goals 5. Ftactic.goals -> Ftactic.nf_goals 6. Ftactic.raw_goals -> Ftactic.goals This is more uniform with the other functions of Coq.
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
|
* At last a working clearbody!Gravatar Pierre-Marie Pédrot2014-09-05
| | | | | | | This time it should work at least as well as the previous version. The error messages were adapted a little. There is still a buggy behaviour when clearing lets in section, but this is mostly a problem of section handling. The v8.4 version of clearbody did exhibit the same behaviour anyway.
* Only using filtered hyps in Goal.enter.Gravatar Pierre-Marie Pédrot2014-09-04
| | | | | This was probably a bug. A user-side code should never be able to observe the difference between filtered and unfiltered hypotheses.
* Ensuring the invariant that hypotheses and named context of the environment ofGravatar Pierre-Marie Pédrot2014-09-04
| | | | | Proofview goals coincide by always using the named context and discarding the hypotheses.
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
|
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
|
* Fix: shelve_unifiable did not work modulo evar instantiation.Gravatar Arnaud Spiwack2014-09-04
| | | Irony…
* Proofview refiner is now type-safe by default.Gravatar Pierre-Marie Pédrot2014-09-04
| | | | | | | | | In order not to be too costly, there is an [unsafe] flag to be set if the tactic does not have to check that the partial proof term is well-typed (to be used with caution though). This patch breaks one [fix]-based example in the refine test-suite, but a huge development like CompCert still goes through.
* Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Gravatar Pierre-Marie Pédrot2014-09-04
| | | | Hopefully, this may fix some nasty bugs lying around.
* Using goal-tactics to interpret arguments to idtac.Gravatar Pierre-Marie Pédrot2014-09-04
| | | | | | This allows to write a multigoal idtac without having to resort to the hack of modifying the global environment tactic through tclIN_ENV, which may cause trouble if we want to modify it in a state-passing style.
* Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Gravatar Pierre-Marie Pédrot2014-09-04
| | | | | | | This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6. Conflicts: proofs/proofview.ml
* Putting back normalized goals when entering them.Gravatar Pierre-Marie Pédrot2014-09-03
| | | | | This should allow tactics after a Goal.enter not to have to renormalize them uselessly.
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
| | | | | | | | | | | now done entirely using declare_mind, which declares the associated constants for primitive records. This avoids a hack related to elimination schemes and ensures that the forward references to constants in the mutual inductive entry are properly declared just after the inductive. This also clarifies (and simplifies) the code of term_typing for constants which does not have to deal with building or checking projections anymore. Also fix printing of universes showing the de Bruijn encoding in a few places.
* Simplification of the tclCHECKINTERRUPT tactic.Gravatar Pierre-Marie Pédrot2014-08-28
|
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
| | | | | | | | | | | Now kernel/indtypes builds the corresponding terms (has to be trusted) while translate_constant just binds a constant name to the already entered projection body, avoiding the dubious "check" of user given terms. "case" Pattern-matching on primitive records is now disallowed, and the default scheme is implemented using projections and eta (all elimination tactics now use projections as well). Elaborate "let (x, y) := p in t" using let bindings for the projections of p too.
* Cleaning and documenting a bit the Proofview.Refine module.Gravatar Pierre-Marie Pédrot2014-08-28
|
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
|
* Removing unused parts of the Goal.sensitive monad.Gravatar Pierre-Marie Pédrot2014-08-21
| | | | | | Some legacy code remains to keep the newish refine tactic working, but ultimately it should be removed. I did not manage to do it properly though, i.e. without breaking the test-suite furthermore.
* Removing a use of Goal.refine.Gravatar Pierre-Marie Pédrot2014-08-19
|
* New primitive allowing to modify refine handles.Gravatar Pierre-Marie Pédrot2014-08-19
|
* Improving error message when applying rewrite to an expression which is not ↵Gravatar Hugo Herbelin2014-08-18
| | | | an equality.
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
| | | | | | | | | - made "apply" tactics of type Proofview.tactic, as well as other inner functions about elim and assert - used same hypothesis naming policy for intros and internal_cut (towards a reorganization of intro patterns) - "apply ... in H as pat" now supports any kind of introduction pattern (doc not changed)
* More self-contained code for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
|
* 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).
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 03:13:30 +0000