aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-09-07Fixing bug #3492.Pierre-Marie Pédrot
2014-09-06Inlining code in Tacinterp that was only used once.Pierre-Marie Pédrot
2014-09-06Code simplification in Tacinterp.Pierre-Marie Pédrot
2014-09-06Proper interpretation function for tauto.Pierre-Marie Pédrot
Instead of passing glob tactics through the infamous globTacticIn hack and antiquotation feature of the Ltac syntax, we put them in the interpretation environment as closures. This should be used everywhere to get rid of this buggy antiquotation syntax. This fixes bug #2800.
2014-09-06Adding a way to inject tactic closures in interpretation values.Pierre-Marie Pédrot
2014-09-06Fixing clearbody : typecheck definitions in context.Pierre-Marie Pédrot
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
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.
2014-09-06Fix bug #3584, elaborating pattern-matching on primitive records to theMatthieu Sozeau
use of projections.
2014-09-06Remove debug printing codeMatthieu Sozeau
2014-09-06Cleanup code for looking up projection bodies.Matthieu Sozeau
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly,Matthieu Sozeau
simplifying conversion code.
2014-09-06Fix checker to handle projections with eta and universe polymorphism correctly.Matthieu Sozeau
2014-09-06Fix checking of constants in checker. Prelude can now be checked.Matthieu Sozeau
2014-09-05Remove unused substitution functions in checker.Matthieu Sozeau
2014-09-05Fix checker treatment of inductives using subst_instances instead of ↵Matthieu Sozeau
subst_univs_levels.
2014-09-05Retype terms resulting from the feeding of a context with a term.Pierre-Marie Pédrot
Fixes bug #3455.
2014-09-05Fix checker/values.ml with latest changes due to projections and universes.Matthieu Sozeau
2014-09-05Remove a redundant typing phase in the [refine] tactic.Arnaud Spiwack
The refined term is still typechecked twice (not counting Qed). But there seem to be a bug in the typechecker whereby it sometimes return terms which have universe inconsistencies. Until this is fixed, I'll leave the second typing phase which seems to catch these inconsistencies. To remove it, it suffices to change the [unsafe] flag to [true].
2014-09-05Silence an ocaml warning.Arnaud Spiwack
2014-09-05The pretyping of [uconstr] in [refine] uses the identifier of the ltac ↵Arnaud Spiwack
context for goal contexts.
2014-09-05Ltac's [uconstr] values now use the identifier context to give names to binders.Arnaud Spiwack
It does not work fine for refine yet as, while the binder has indeed the correct name, the evars are pretyped in an environment with the Ltac name, hence goal do not display the appropriate name.
2014-09-05Adds an identifier context in pretying's Ltac context.Arnaud Spiwack
Binder names are interpreted as the Ltac specified one if available.
2014-09-05Fix parsing of "subterm(s)" strategy argument.Matthieu Sozeau
2014-09-05Rename eta_expand_ind_stacks, fix the one from the checker and adaptMatthieu Sozeau
it to the new representation of projections and the new mind_finite type.
2014-09-05Adding a Ftactic module for potentially focussing tactics.Pierre-Marie Pédrot
The code for the module was moved from Tacinterp. We still expose partially the implementation of the Ftactic.t type, for the sake of simplicity. It may be dangerous if used improperly though.
2014-09-05Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-05Fix primitive projections declarations for inductive records.Matthieu Sozeau
2014-09-05At last a working clearbody!Pierre-Marie Pédrot
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.
2014-09-04Only using filtered hyps in Goal.enter.Pierre-Marie Pédrot
This was probably a bug. A user-side code should never be able to observe the difference between filtered and unfiltered hypotheses.
2014-09-04Ensuring the invariant that hypotheses and named context of the environment ofPierre-Marie Pédrot
Proofview goals coincide by always using the named context and discarding the hypotheses.
2014-09-04Revert the two previous commits. I was testing in the wrong branch.Pierre-Marie Pédrot
2014-09-04Removing the old implementation of clear_body.Pierre-Marie Pédrot
2014-09-04Reimplementing the clearbody tactic.Pierre-Marie Pédrot
2014-09-04Make CoqIDE compile with windows (Closes: 3573)Enrico Tassi
CoqIDE seems to work, but for random pauses that make you think of a thread deadlock, but then, after a few seconds, things make progress again. This happens only seldom on my virtual machine.
2014-09-04Fix: shelve_unifiable did not work modulo evar instantiation.Arnaud Spiwack
Irony…
2014-09-04Proofview refiner is now type-safe by default.Pierre-Marie Pédrot
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.
2014-09-04Typing.sort_of does not leak evarmaps anymore.Pierre-Marie Pédrot
2014-09-04More explicit printing in Himsg.Pierre-Marie Pédrot
2014-09-04Status error for bug #3459.Pierre-Marie Pédrot
2014-09-04Test for bug #3459.Pierre-Marie Pédrot
2014-09-04Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Pierre-Marie Pédrot
Hopefully, this may fix some nasty bugs lying around.
2014-09-04Using goal-tactics to interpret arguments to idtac.Pierre-Marie Pédrot
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.
2014-09-04Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Pierre-Marie Pédrot
This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6. Conflicts: proofs/proofview.ml
2014-09-04Revert "Tacinterp: [interp_message] and associate now only require an ↵Pierre-Marie Pédrot
environment rather than an entire goal." This reverts commit 4eaafcd00992302c186b8d11e890616726ebd822.
2014-09-04Revert "Ltac's idtac is now implemented using the new API."Pierre-Marie Pédrot
This reverts commit 5b92ff7b0a641bf2daa31b60bf49b57a5d1e8452.
2014-09-04Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."Pierre-Marie Pédrot
This reverts commit afa441019432f70245fed6adc5eb0318514e4357.
2014-09-04Fix bug #3561, correct folding of env in context[] matching.Matthieu Sozeau
2014-09-04Fix bug #3559, ensuring a canonical order of universe level quantifications whenMatthieu Sozeau
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one used before introduction of hMaps in LMap/LSet.
2014-09-04Documenting the [Variant] type definition and the [Nonrecursive Elimination ↵Arnaud Spiwack
Schemes] option.
2014-09-04Commands like [Inductive > X := … | … | …] raise an error message ↵Arnaud Spiwack
instead of silently ignoring the ">" syntax.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-18 08:16:49 +0000