aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fixing typo absorption (bug #3751).Gravatar Hugo Herbelin2014-10-22
|
* Proofview: documentation and re-ordering.Gravatar Arnaud Spiwack2014-10-22
|
* Split [Proofview] into a file where the basic operations on the state are ↵Gravatar Arnaud Spiwack2014-10-22
| | | | | | 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.
* Make names in [Proofview_monad] more uniform.Gravatar Arnaud Spiwack2014-10-22
| | | | 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.
* Proofview: remove and inline [on_advance] function.Gravatar Arnaud Spiwack2014-10-22
| | | | [on_advance] gave almost no gain in readability, while costing a closure.
* Proofview: add a lens for the evar_map and factor some code.Gravatar Arnaud Spiwack2014-10-22
|
* Proofview: use an iter-like combinator rather than a fold_left-like one for ↵Gravatar Arnaud Spiwack2014-10-22
| | | | | | dispatch. Leads to clearer an more efficient code.
* An additional [List.iter] monadic combinator.Gravatar Arnaud Spiwack2014-10-22
|
* Add more primitives to the [Monad.Make] arguments.Gravatar Arnaud Spiwack2014-10-22
| | | | For optimisation purposes.
* Improve readability the "lenses" in Proofview, using interfaces.Gravatar Arnaud Spiwack2014-10-22
|
* Proofview: clean up code a little.Gravatar Arnaud Spiwack2014-10-22
|
* Proofview: move [list_goto] to the [CList] module.Gravatar Arnaud Spiwack2014-10-22
| | | | It is, after all, a generic function about lists.
* Proofview: replace the functions iter_list and iter_list2 by generic monadic ↵Gravatar Arnaud Spiwack2014-10-22
| | | | combinators.
* Add a two-list monadic fold_left iterator.Gravatar Arnaud Spiwack2014-10-22
|
* Small optimisation in the monadic list combinators.Gravatar Arnaud Spiwack2014-10-22
| | | | 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.
* Factor module signatures.Gravatar Arnaud Spiwack2014-10-22
|
* Proofview: clean up commented out code.Gravatar Arnaud Spiwack2014-10-22
|
* Proofview: remove a redundant primitive.Gravatar Arnaud Spiwack2014-10-22
|
* Proofview: move more functions to the Unsafe module.Gravatar Arnaud Spiwack2014-10-22
|
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
| | | | 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.
* Proofview.mli: no more reference to Goal.goal.Gravatar Arnaud Spiwack2014-10-22
|
* Proofview: factor init and dependent_init.Gravatar Arnaud Spiwack2014-10-22
|
* Remove unused functions for side effects.Gravatar Arnaud Spiwack2014-10-22
|
* Remove the deprecated open-constr based refine.Gravatar Arnaud Spiwack2014-10-22
| | | | | | | | 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.
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
| | | As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
* Remove duplicate code.Gravatar Arnaud Spiwack2014-10-22
|
* Removing dead code in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
|
* Small invariants in Rewrite code.Gravatar Pierre-Marie Pédrot2014-10-21
|
* Lazily check that an argument is dependent when constructing evar clauses.Gravatar Pierre-Marie Pédrot2014-10-21
|
* Fixing decompose_app_rel in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
| | | | | The old implementation did not beta-iota normalize before observing the head of the term, resulting in stange bugs.
* Using new clausenv in rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
|
* Adding an evar version of the make_clenv function.Gravatar Pierre-Marie Pédrot2014-10-21
|
* Porting Hugo's fix 98f3abb83a to native compiler.Gravatar Maxime Dénès2014-10-21
|
* Adapting output tests to the removal of the new token warning and toGravatar Hugo Herbelin2014-10-21
| | | | the printing of the context of open evars in Check.
* More precise test for #3459.Gravatar Hugo Herbelin2014-10-21
|
* Dead code.Gravatar Hugo Herbelin2014-10-21
|
* Continuing experimental printing of the signature of open evars inGravatar Hugo Herbelin2014-10-21
| | | | | | 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].
* Removing re-typecheking from "refine" in no-check mode of the newGravatar Hugo Herbelin2014-10-20
| | | | | | 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.
* Fixing a (new) part of bug #2729.Gravatar Hugo Herbelin2014-10-20
| | | | | | | | | | | 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).
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
| | | | | | | | | | | 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.
* Fixing a bug in the presence of let-in in inductive arity.Gravatar Hugo Herbelin2014-10-20
|
* Revert "Fixing a loop in proof reconstruction for congruence (#2447)."Gravatar Hugo Herbelin2014-10-17
| | | | | | | committed by mistake. The message pretended to have a fix which is only superficially a fix. The problem is more complex. This reverts commit 251218905daea0838a3738466afa1c278bb3e81b.
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une ↵Gravatar Hugo Herbelin2014-10-17
| | | | | | équation;" which was committed by mistake. This reverts commit a53b44aa042cfded28c34205074f194de7e2e4ee.
* Now printing "now a keyword" only in verbose mode.Gravatar Hugo Herbelin2014-10-17
|
* When facing problem ?id = ?id' in resolution of return predicate,Gravatar Hugo Herbelin2014-10-17
| | | | | | early call the standard resolution function which e.g. does restriction and maybe solve the problem if pattern-like, instead of postponing the problem.
* Experimental printing of the signature of open evars in Check.Gravatar Hugo Herbelin2014-10-17
|
* New experimental heuristic printing strategy for evar instances: WeGravatar Hugo Herbelin2014-10-17
| | | | | | | | | don't print bindings of the form "x:=x" unless there is also a binding "x':=x". Otherwise said, if a variable occurs several time, the binding where it occurs under the form "x:=x" is printed anyway. This should help to understand where the instance is non trivial while still not obfuscating display in goals with very long list of uninteresting trivial instances.
* Re-displaying evar instances in debugger.Gravatar Hugo Herbelin2014-10-17
|
* Fixing a loop in proof reconstruction for congruence (#2447).Gravatar Hugo Herbelin2014-10-17
| | | | | | | | | | | | | | Proofs of C t1..tn+1 = C t1..tn+1, even when the terms were syntactically the same, were built by composition of a proof of C t1..tn = C t1..tn with a proof of reflexivity of tn+1. The latter was reduced to showing C t1..tn = C u1..un for C u1..un the canonical representant of C t1..tn in its congruence class. But if some pair ti=ui was derivable by injectivity of the constructor C, it might go back to find a proof of C t1..tn+1 = C t1..tn+1 again, while a simple reflexivity proof was enough here. Not sure that the fix prevents any further loop in this part of the code though.
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 02:15:04 +0000