| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2014-09-02 | Another fix than 19a7a5789c to avoid descend_in_conjunction to use | Hugo Herbelin | |
| fresh names interferring with names later generated in intropatterns (as introduced in 72498d6d68ac which passed "clenv_refine_in continued by pattern introduction" to descend_in_conjunction while only a pure clenv_refine was passed before). The 72498d6d68ac version was generating fresh names in the wrong order (morally-private names for descend_in_conjunction before user-level names in clenv_refine_in). The 19a7a5789c fix was introducing expressions not handled by the refine from logic.ml. In particular, this fixes RelationAlgebra. | |||
| 2014-09-02 | An apply test. | Hugo Herbelin | |
| 2014-09-02 | Fixup introduction of coqworkmgr | Pierre Boutillier | |
| 2014-09-02 | Removing [revert] tactic from the AST. | Pierre-Marie Pédrot | |
| 2014-09-02 | stm: use xlabel insted of label in dot (debug) output | Enrico Tassi | |
| 2014-09-02 | coqworkmgr | Enrico Tassi | |
| 2014-09-02 | Fix Declaremods.end_library (Closes: #3536) | Enrico Tassi | |
| 2014-09-01 | Removing the 'inductive' parameter from tacexpr AST. | Pierre-Marie Pédrot | |
| It was actually useless, because its only use was in the moved away decompose tactic. | |||
| 2014-09-01 | Moving the decompose tactic out of the AST. | Pierre-Marie Pédrot | |
| 2014-09-01 | In evarconv, do first-order unification of LetIn's properly, ensuring we ↵ | Matthieu Sozeau | |
| compare bodies of convertible types! Bug found by B. Ziliani. | |||
| 2014-09-01 | Coqide prints succesive hyps of the same type on 1 line | Pierre Boutillier | |
| This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses don't respect Barendregt convention". | |||
| 2014-09-01 | Code cleaning in Tacintern. | Pierre-Marie Pédrot | |
| 2014-08-31 | Getting rid of atomic tactics in Tacenv. | Pierre-Marie Pédrot | |
| ML tactics that may be used as simple identifiers are now declared as a true Ltac entry pertaining to the module that contains the Declare ML Module statement. | |||
| 2014-08-31 | Moving code of tactic interpretation from Tacenv to Vernacentries. | Pierre-Marie Pédrot | |
| This allows to directly register globtactics in the Tacenv API, without having to resort to any internalization function. | |||
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau | |
| 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. | |||
| 2014-08-29 | Type-safe version of genarg list / pair / opt functions. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |