| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-09-05 | Fix checker/values.ml with latest changes due to projections and universes. | Matthieu Sozeau | |
| 2014-09-05 | Remove 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-05 | Silence an ocaml warning. | Arnaud Spiwack | |
| 2014-09-05 | The pretyping of [uconstr] in [refine] uses the identifier of the ltac ↵ | Arnaud Spiwack | |
| context for goal contexts. | |||
| 2014-09-05 | Ltac'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-05 | Adds an identifier context in pretying's Ltac context. | Arnaud Spiwack | |
| Binder names are interpreted as the Ltac specified one if available. | |||
| 2014-09-05 | Fix parsing of "subterm(s)" strategy argument. | Matthieu Sozeau | |
| 2014-09-05 | Rename eta_expand_ind_stacks, fix the one from the checker and adapt | Matthieu Sozeau | |
| it to the new representation of projections and the new mind_finite type. | |||
| 2014-09-05 | Adding 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-05 | Removing the old implementation of clear_body. | Pierre-Marie Pédrot | |
| 2014-09-05 | Fix primitive projections declarations for inductive records. | Matthieu Sozeau | |
| 2014-09-05 | At 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-04 | Only 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-04 | Ensuring the invariant that hypotheses and named context of the environment of | Pierre-Marie Pédrot | |
| Proofview goals coincide by always using the named context and discarding the hypotheses. | |||
| 2014-09-04 | Revert the two previous commits. I was testing in the wrong branch. | Pierre-Marie Pédrot | |
| 2014-09-04 | Removing the old implementation of clear_body. | Pierre-Marie Pédrot | |
| 2014-09-04 | Reimplementing the clearbody tactic. | Pierre-Marie Pédrot | |
| 2014-09-04 | Make 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-04 | Fix: shelve_unifiable did not work modulo evar instantiation. | Arnaud Spiwack | |
| Irony… | |||
| 2014-09-04 | Proofview 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-04 | Typing.sort_of does not leak evarmaps anymore. | Pierre-Marie Pédrot | |
| 2014-09-04 | More explicit printing in Himsg. | Pierre-Marie Pédrot | |
| 2014-09-04 | Status error for bug #3459. | Pierre-Marie Pédrot | |
| 2014-09-04 | Test for bug #3459. | Pierre-Marie Pédrot | |
| 2014-09-04 | Adding 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-04 | Using 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-04 | Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]." | Pierre-Marie Pédrot | |
| This reverts commit 664b3cba1e8d326382ca981aa49fdf00edd429e6. Conflicts: proofs/proofview.ml | |||
| 2014-09-04 | Revert "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-04 | Revert "Ltac's idtac is now implemented using the new API." | Pierre-Marie Pédrot | |
| This reverts commit 5b92ff7b0a641bf2daa31b60bf49b57a5d1e8452. | |||
| 2014-09-04 | Revert "Ltac's [idtac] is now interpreted outside of a goal if possible." | Pierre-Marie Pédrot | |
| This reverts commit afa441019432f70245fed6adc5eb0318514e4357. | |||
| 2014-09-04 | Fix bug #3561, correct folding of env in context[] matching. | Matthieu Sozeau | |
| 2014-09-04 | Fix bug #3559, ensuring a canonical order of universe level quantifications when | Matthieu 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-04 | Documenting the [Variant] type definition and the [Nonrecursive Elimination ↵ | Arnaud Spiwack | |
| Schemes] option. | |||
| 2014-09-04 | Commands like [Inductive > X := … | … | …] raise an error message ↵ | Arnaud Spiwack | |
| instead of silently ignoring the ">" syntax. | |||
| 2014-09-04 | Factorize the parsing rules of [Record] and the other kind of type definitions. | Arnaud Spiwack | |
| They were almost identical, except some unused misplaced coercion symbol in the non-[Record] rule. | |||
| 2014-09-04 | Remove [Infer] option of records. | Arnaud Spiwack | |
| Dead code formerly used by the now defunct [autoinstances]. | |||
| 2014-09-04 | Type definitions with [Variant] don't generate inductive schemes by default. | Arnaud Spiwack | |
| - The option [Record Elimination Schemes] is replaced by [Nonrecursive Elimination Schemes] ([Record Elimination Schemes] is kept as a deprecated option for compatibility) - [Variant] don't generate inductive scheme unless [Nonrecursive Elimination Schemes] is turned on. - Inductive records generate induction schemes even when [Nonrecursive Elimination Schemes] is off. | |||
| 2014-09-04 | Type definitions [Variant] and [Record] really don't accept the wrong kind ↵ | Arnaud Spiwack | |
| of definition. - [Variant] will accept variant definitions but no record definition - [Record] will accept record definitions but no variant definition | |||
| 2014-09-04 | Inductive and CoInductive records are printed correctly. | Arnaud Spiwack | |
| 2014-09-04 | Types declared as Variants really do not accept recursive definitions. | Arnaud Spiwack | |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack | |
| Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced. | |||
| 2014-09-04 | Add a [Variant] declaration which allows to write non-recursive variant types. | Arnaud Spiwack | |
| Just like the [Record] keyword allows only non-recursive records. | |||
| 2014-09-04 | Add test-suite file for Case derivation on primitive records. | Matthieu Sozeau | |
| 2014-09-04 | Add test suite files for closed bugs. | Matthieu Sozeau | |
| 2014-09-04 | Fix bug #3563, making syntactic matching of primitive projections | Matthieu Sozeau | |
| and their eta-expanded forms succeed, potentially filling parameter metavariables from the type information of the projected object. | |||
| 2014-09-03 | Putting back normalized goals when entering them. | Pierre-Marie Pédrot | |
| This should allow tactics after a Goal.enter not to have to renormalize them uselessly. | |||
| 2014-09-03 | Yes another remaining clearing bug with 'apply in'. | Hugo Herbelin | |
| 2014-09-03 | Fixing printing of unreachable local tactics. | Pierre-Marie Pédrot | |
| 2014-09-03 | Test-suite for bug #2818. | Pierre-Marie Pédrot | |
| 2014-09-03 | Fixing bug #2818. | Pierre-Marie Pédrot | |
| Local Ltac definitions do not register their name in the nametab anymore, thus elegantly solving the bug. The tactic body remains accessible from the tactic engine, but the name is rendered meaningless to the userside. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |