aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Status error for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
|
* Test for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
|
* 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
* Revert "Tacinterp: [interp_message] and associate now only require an ↵Gravatar Pierre-Marie Pédrot2014-09-04
| | | | | | environment rather than an entire goal." This reverts commit 4eaafcd00992302c186b8d11e890616726ebd822.
* Revert "Ltac's idtac is now implemented using the new API."Gravatar Pierre-Marie Pédrot2014-09-04
| | | | This reverts commit 5b92ff7b0a641bf2daa31b60bf49b57a5d1e8452.
* Revert "Ltac's [idtac] is now interpreted outside of a goal if possible."Gravatar Pierre-Marie Pédrot2014-09-04
| | | | This reverts commit afa441019432f70245fed6adc5eb0318514e4357.
* Fix bug #3561, correct folding of env in context[] matching.Gravatar Matthieu Sozeau2014-09-04
|
* Fix bug #3559, ensuring a canonical order of universe level quantifications whenGravatar Matthieu Sozeau2014-09-04
| | | | | introducing constants (e.g. Top.1 is always before Top.2), compatible with the one used before introduction of hMaps in LMap/LSet.
* Documenting the [Variant] type definition and the [Nonrecursive Elimination ↵Gravatar Arnaud Spiwack2014-09-04
| | | | Schemes] option.
* Commands like [Inductive > X := … | … | …] raise an error message ↵Gravatar Arnaud Spiwack2014-09-04
| | | | instead of silently ignoring the ">" syntax.
* Factorize the parsing rules of [Record] and the other kind of type definitions.Gravatar Arnaud Spiwack2014-09-04
| | | | They were almost identical, except some unused misplaced coercion symbol in the non-[Record] rule.
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
| | | Dead code formerly used by the now defunct [autoinstances].
* Type definitions with [Variant] don't generate inductive schemes by default.Gravatar Arnaud Spiwack2014-09-04
| | | | | | - 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.
* Type definitions [Variant] and [Record] really don't accept the wrong kind ↵Gravatar Arnaud Spiwack2014-09-04
| | | | | | | of definition. - [Variant] will accept variant definitions but no record definition - [Record] will accept record definitions but no variant definition
* Inductive and CoInductive records are printed correctly.Gravatar Arnaud Spiwack2014-09-04
|
* Types declared as Variants really do not accept recursive definitions.Gravatar Arnaud Spiwack2014-09-04
|
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
| | | | 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.
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
| | | | Just like the [Record] keyword allows only non-recursive records.
* Add test-suite file for Case derivation on primitive records.Gravatar Matthieu Sozeau2014-09-04
|
* Add test suite files for closed bugs.Gravatar Matthieu Sozeau2014-09-04
|
* Fix bug #3563, making syntactic matching of primitive projectionsGravatar Matthieu Sozeau2014-09-04
| | | | | and their eta-expanded forms succeed, potentially filling parameter metavariables from the type information of the projected object.
* 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.
* Yes another remaining clearing bug with 'apply in'.Gravatar Hugo Herbelin2014-09-03
|
* Fixing printing of unreachable local tactics.Gravatar Pierre-Marie Pédrot2014-09-03
|
* Test-suite for bug #2818.Gravatar Pierre-Marie Pédrot2014-09-03
|
* Fixing bug #2818.Gravatar Pierre-Marie Pédrot2014-09-03
| | | | | | 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.
* Useless hooks in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
|
* Code simplification in Tacenv.Gravatar Pierre-Marie Pédrot2014-09-03
|
* Print error messages with more hidden information based on α-equivalence .Gravatar Arnaud Spiwack2014-09-03
| | | | | 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.
* sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.texGravatar Pierre Boutillier2014-09-03
|
* Improve RefMan section about Coq_makefileGravatar Pierre Boutillier2014-09-03
|
* Update RefMan with respect to new loadpath managementGravatar Pierre Boutillier2014-09-03
|
* Cbn in refmanGravatar Pierre Boutillier2014-09-03
|
* Additional entry tactic_arg in Print Grammar tactic.Gravatar Pierre-Marie Pédrot2014-09-03
|
* Code factorization in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
|
* Cleaning code in Pptactic.Gravatar Pierre-Marie Pédrot2014-09-02
| | | | | | 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.
* Adding a test-suite for second-order matching order and indexes.Gravatar Pierre-Marie Pédrot2014-09-02
|
* Fixing bug #3136.Gravatar Pierre-Marie Pédrot2014-09-02
| | | | Second-order pattern-matching now respect variable abstraction order.
* Another fix than 19a7a5789c to avoid descend_in_conjunction to useGravatar Hugo Herbelin2014-09-02
| | | | | | | | | | | | | 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.
* An apply test.Gravatar Hugo Herbelin2014-09-02
|
* Fixup introduction of coqworkmgrGravatar Pierre Boutillier2014-09-02
|
* Removing [revert] tactic from the AST.Gravatar Pierre-Marie Pédrot2014-09-02
|
* stm: use xlabel insted of label in dot (debug) outputGravatar Enrico Tassi2014-09-02
|
* coqworkmgrGravatar Enrico Tassi2014-09-02
|
* Fix Declaremods.end_library (Closes: #3536)Gravatar Enrico Tassi2014-09-02
|
* Removing the 'inductive' parameter from tacexpr AST.Gravatar Pierre-Marie Pédrot2014-09-01
| | | | | It was actually useless, because its only use was in the moved away decompose tactic.
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
|
* In evarconv, do first-order unification of LetIn's properly, ensuring we ↵Gravatar Matthieu Sozeau2014-09-01
| | | | | | compare bodies of convertible types! Bug found by B. Ziliani.
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-27 22:42:51 +0000