| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-22 | Fix missing lift in VM and native compiler (second part of #2729). | Maxime Dénès | |
| Was occurring in the parameters of constructors when reifying a dependent pattern matching return predicate. Note: this does not affect the kernel, only the pretyper. | |||
| 2014-10-22 | Refine tactic: simplify the conclusion only at the end of the tactic. | Arnaud Spiwack | |
| It was the intended semantics from the beginning. I just wrote it wrong. Spotted by Hugo, fix by Hugo. | |||
| 2014-10-22 | Oversight in ce260a0db279ce09dda70e079ae3c35b49f05ec4 (Proper scoping of ↵ | Arnaud Spiwack | |
| future goals). Fixes #3757. Thanks to Hugo for helping pinpoint the issue. | |||
| 2014-10-22 | Remove an unnecessary use of [Proofview.Unsafe.tclEVARS] in [convert_concl]. | Arnaud Spiwack | |
| 2014-10-22 | EqdepFacts: generalize statements which were wrongly restricted to Prop. | Arnaud Spiwack | |
| 2014-10-22 | CHANGES: makes explicit the incompatibily introduced by the use of ↵ | Arnaud Spiwack | |
| Ltac-defined names in term binders. Closes #3747. | |||
| 2014-10-22 | Fixing an evar leak in pattern-matching compilation (#3758). | Hugo Herbelin | |
| 2014-10-22 | Fixing what really looks like a bug in the initial implementation of | Hugo Herbelin | |
| coqdoc links for modules (#3756). | |||
| 2014-10-22 | Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers. | Hugo Herbelin | |
| 2014-10-22 | Fixing typo absorption (bug #3751). | Hugo Herbelin | |
| 2014-10-22 | Proofview: documentation and re-ordering. | Arnaud Spiwack | |
| 2014-10-22 | Split [Proofview] into a file where the basic operations on the state are ↵ | Arnaud Spiwack | |
| defined and the file providing the primitives. The datatypes are defined in [Proofview_monad], previous [Proofview_monad] is now called [Logic_monad] since it is more generic since the refactoring. | |||
| 2014-10-22 | Make names in [Proofview_monad] more uniform. | Arnaud Spiwack | |
| ret -> return, bind -> (>>=), etc… So that monads expose a [Monad.S] signature. Also Proofview now exposes the [Monad.S] signature directly rather than in a [Monad.S] subdirectory. | |||
| 2014-10-22 | Proofview: remove and inline [on_advance] function. | Arnaud Spiwack | |
| [on_advance] gave almost no gain in readability, while costing a closure. | |||
| 2014-10-22 | Proofview: add a lens for the evar_map and factor some code. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: use an iter-like combinator rather than a fold_left-like one for ↵ | Arnaud Spiwack | |
| dispatch. Leads to clearer an more efficient code. | |||
| 2014-10-22 | An additional [List.iter] monadic combinator. | Arnaud Spiwack | |
| 2014-10-22 | Add more primitives to the [Monad.Make] arguments. | Arnaud Spiwack | |
| For optimisation purposes. | |||
| 2014-10-22 | Improve readability the "lenses" in Proofview, using interfaces. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: clean up code a little. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: move [list_goto] to the [CList] module. | Arnaud Spiwack | |
| It is, after all, a generic function about lists. | |||
| 2014-10-22 | Proofview: replace the functions iter_list and iter_list2 by generic monadic ↵ | Arnaud Spiwack | |
| combinators. | |||
| 2014-10-22 | Add a two-list monadic fold_left iterator. | Arnaud Spiwack | |
| 2014-10-22 | Small optimisation in the monadic list combinators. | Arnaud Spiwack | |
| The monadic bind can be costly, so sparing a few can be worth it. Therefore I unrolled the last element of the recursions. I took the opportunity to do some loop unrolling, which is probably more useful for map combinators than for fold. | |||
| 2014-10-22 | Factor module signatures. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: clean up commented out code. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: remove a redundant primitive. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: move more functions to the Unsafe module. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: split [V82] module into [Unsafe] and [V82]. | Arnaud Spiwack | |
| The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function. | |||
| 2014-10-22 | Proofview.mli: no more reference to Goal.goal. | Arnaud Spiwack | |
| 2014-10-22 | Proofview: factor init and dependent_init. | Arnaud Spiwack | |
| 2014-10-22 | Remove unused functions for side effects. | Arnaud Spiwack | |
| 2014-10-22 | Remove the deprecated open-constr based refine. | Arnaud Spiwack | |
| That is [Tactics.New.refine]. Replaced it with a wrapper around the primitive refine [Proofview.Refine.refine], but with extra reductions on the resulting goals. There was two used of this refine: one in the declarative mode, and one in type classes. The porting of the latter is likely to have introduced bugs. Factored code with Ltac's refine in Extratactics. | |||
| 2014-10-22 | Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs. | Arnaud Spiwack | |
| As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left. | |||
| 2014-10-22 | Remove duplicate code. | Arnaud Spiwack | |
| 2014-10-21 | Removing dead code in Rewrite. | Pierre-Marie Pédrot | |
| 2014-10-21 | Small invariants in Rewrite code. | Pierre-Marie Pédrot | |
| 2014-10-21 | Lazily check that an argument is dependent when constructing evar clauses. | Pierre-Marie Pédrot | |
| 2014-10-21 | Fixing decompose_app_rel in Rewrite. | Pierre-Marie Pédrot | |
| The old implementation did not beta-iota normalize before observing the head of the term, resulting in stange bugs. | |||
| 2014-10-21 | Using new clausenv in rewrite. | Pierre-Marie Pédrot | |
| 2014-10-21 | Adding an evar version of the make_clenv function. | Pierre-Marie Pédrot | |
| 2014-10-21 | Porting Hugo's fix 98f3abb83a to native compiler. | Maxime Dénès | |
| 2014-10-21 | Adapting output tests to the removal of the new token warning and to | Hugo Herbelin | |
| the printing of the context of open evars in Check. | |||
| 2014-10-21 | More precise test for #3459. | Hugo Herbelin | |
| 2014-10-21 | Dead code. | Hugo Herbelin | |
| 2014-10-21 | Continuing experimental printing of the signature of open evars in | Hugo Herbelin | |
| Check (see cfff8f8a327) [printing only visible evars, not the ones corresponding to unrelated open goals + fixing bug on wrong sigma and on evar_info normalization]. | |||
| 2014-10-20 | Removing re-typecheking from "refine" in no-check mode of the new | Hugo Herbelin | |
| convert_concl/convert_hyp. This was actually probably the main source of inefficiency introduced on Oct 9 (see e.g. CoLoR), rather than nf_enter, as suspected in 3c2723f. | |||
| 2014-10-20 | Fixing a (new) part of bug #2729. | Hugo Herbelin | |
| By moving convert_concl to new proof engine, re-typecheckeing was incidentally introduced. Re-typechecking revealed that vm bug #2729 was still open. Indeed, the vm was still producing an ill-typed term. This commit fixes ill-typedness of the vm in #2729 when reconstructing a "match" in an inductive type whose constructors have let-ins. Another part is still open (see test-suite). | |||
| 2014-10-20 | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin | |
| but the internal representation dropped let-in. Ideally, the internal representation of the "match" should use contexts for the predicate and the branches. This would however be a rather significant change. In the meantime, just a hack. To do, there is still an extra @ in the constructor name that does not need to be there. | |||
| 2014-10-20 | Fixing a bug in the presence of let-in in inductive arity. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |