| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2014-09-03 | Useless hooks in Tacintern. | Pierre-Marie Pédrot | |
| 2014-09-03 | Code simplification in Tacenv. | Pierre-Marie Pédrot | |
| 2014-09-03 | Print error messages with more hidden information based on α-equivalence . | Arnaud Spiwack | |
| The comparison on terms which triggers new printing flags in case two terms which are different would be printed identically now contains α-equivalence. The implementation using a canonization function on [constr] instead of trying to deal with [constr_expr] was suggested by Hugo. | |||
| 2014-09-03 | sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex | Pierre Boutillier | |
| 2014-09-03 | Improve RefMan section about Coq_makefile | Pierre Boutillier | |
| 2014-09-03 | Update RefMan with respect to new loadpath management | Pierre Boutillier | |
| 2014-09-03 | Cbn in refman | Pierre Boutillier | |
| 2014-09-03 | Additional entry tactic_arg in Print Grammar tactic. | Pierre-Marie Pédrot | |
| 2014-09-03 | Code factorization in Tacintern. | Pierre-Marie Pédrot | |
| 2014-09-02 | Cleaning code in Pptactic. | Pierre-Marie Pédrot | |
| Parametric printers are now using a record to ease the error reporting when modificating code. Further improvement may include the use of the object layer of OCaml, which would fit in this particular context. | |||
| 2014-09-02 | Adding a test-suite for second-order matching order and indexes. | Pierre-Marie Pédrot | |
| 2014-09-02 | Fixing bug #3136. | Pierre-Marie Pédrot | |
| Second-order pattern-matching now respect variable abstraction order. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |