aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Fixing pervasive equalities. In particular, I removed the code that deletedGravatar Pierre-Marie Pédrot2014-03-03
| | | | | | duplicates in kernel side effects. They were chosen according to an equality that was quite irrelevant, and as expected this patch did not break the test-suite.
* Term dnets do no need to contain the afferent constr pattern in their nodes.Gravatar Pierre-Marie Pédrot2014-03-03
|
* Removing Termdn, and putting the relevant code in Btermdn. The current TermdnGravatar Pierre-Marie Pédrot2014-03-03
| | | | file was useless and duplicated code from Btermdn itself.
* Extruding code not depending of the functor argument in Termdn.Gravatar Pierre-Marie Pédrot2014-03-03
|
* Replacing arguments of Trie by a cancellable monoid.Gravatar Pierre-Marie Pédrot2014-03-03
|
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
| | | | | | | There are currently two other clashs : Lexer and Errors, but for the moment these ones haven't impacted my experiments with extraction and compiler-libs, while this Matching issue had. And anyway the new name is more descriptive, in the spirit of the recent TacticMatching.
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
| | | | | NB: new file miscprint.ml deserves to be part of printing.cma, but should be part of proofs.cma for the moment, due to use in logic.ml
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
|
* Removing a fishy use of pervasive equality in Ltac backtrace printing.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Removing Pervasives.compare in Termdn.Gravatar Pierre-Marie Pédrot2014-02-28
|
* Tacinterp: more refactoring.Gravatar Arnaud Spiwack2014-02-27
| | | Introducing List.fold_right and List.fold_left in Monad.
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
| | | Adds a combinator List.map_right which chains effects from right to left.
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
|
* Remove unsafe code (Obj.magic) in Tacinterp.Gravatar Arnaud Spiwack2014-02-27
| | | This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
* Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Gravatar Arnaud Spiwack2014-02-27
| | | | Impacts MapleMode.
* Get rid of the enterl/glist API for Proofview.Goal.Gravatar Arnaud Spiwack2014-02-27
| | | The prefered style is to use continuation passing style when necessary, or simply passing the goal explicitely in the case of interpretation functions which do not evolve the current goal.
* Tacinterp: yet another superfluous enterl.Gravatar Arnaud Spiwack2014-02-27
|
* Tacinterp: spurious enterl.Gravatar Arnaud Spiwack2014-02-27
| | | This changes the tacinterp API, but only affects (one line of) the MapleMode contrib.
* Dead code: eval_ltac_constr.Gravatar Arnaud Spiwack2014-02-27
|
* Tacinterp: remove the is_value check in Ltac's let-in.Gravatar Arnaud Spiwack2014-02-25
| | | It fixes micromega. It is frankly a mystery to me why psatz ever work. The semantics of Ltac's match is still fishy.
* Tacinterp: fewer enterl still.Gravatar Arnaud Spiwack2014-02-25
|
* Tacinterp: fewer Proofview.Goal.enterl.Gravatar Arnaud Spiwack2014-02-25
| | | | | | | | | | | I'm trying to avoid unecessary construction of intermediate lists. Interpretation function don't modify the goals, they just need a goal in their context. Some care has to be given to the evar maps, though, as we can extract an outdated evar map from a goal (this is probably an undesirable feature, but significantly simplified the compatibility API). Also, Proofview.Goal.enter{,l} catch exceptions (and transfer the non-critical ones into errors of the tactics monad). So I had to do just that for every "enter" removed (I probably have been overprotective but it's better that way). Not as trivial a modification as it should, but it will hopefully go over well. It was much needed anyway.
* Tacinterp: clean up.Gravatar Arnaud Spiwack2014-02-25
|
* Tacinterp: remove unnecessary return/bind pairs.Gravatar Arnaud Spiwack2014-02-25
|
* TacticMatching: avoid some closure allocation in (<*>).Gravatar Arnaud Spiwack2014-02-24
|
* Removed some trailing whitespaces.Gravatar Arnaud Spiwack2014-02-24
|
* IStream: a concat_map primitive.Gravatar Arnaud Spiwack2014-02-24
|
* A view type for IStream.Gravatar Arnaud Spiwack2014-02-24
| | | View types are better practice than option types for pattern-matching. (Plus, they save a minute amount of allocations)
* Removing non-marshallable data from the Agram constructor. Instead ofGravatar Pierre-Marie Pédrot2014-02-16
| | | | | | | | | | containing opaque grammar objects, it now contains a string representing the entry. In order to recover the entry from the string, the former must have been created with [Pcoq.create_generic_entry] or similar. This is guaranteed for entries generated by ARGUMENT EXTEND, and must be done by hand otherwise. Some plugins were fixed accordingly.
* The constructor tactic now returns several successes.Gravatar Pierre-Marie Pédrot2014-02-04
|
* Fixing bug #3226.Gravatar Pierre-Marie Pédrot2014-02-02
|
* In Ltac's exact tactic: avoid checking the type of the term twice.Gravatar Arnaud Spiwack2014-01-31
| | | | Following a remark by Jason Gross and Daniel Grayson.
* Fixing dependent inversion. Some exceptions were not caught by the tacticGravatar Pierre-Marie Pédrot2014-01-28
| | | | monad.
* Adding a default object to generic argument registering mechanism.Gravatar Pierre-Marie Pédrot2014-01-19
|
* Fixing bug #1758: Print Hint output can be misleading if variable shadows ↵Gravatar Pierre-Marie Pédrot2014-01-17
| | | | hypothesis.
* Removing unused tactics in rewrite.Gravatar Pierre-Marie Pédrot2014-01-14
|
* Exporting the full pretyper options in Goal.constr_of_raw.Gravatar Pierre-Marie Pédrot2014-01-10
|
* Fix bug#2080: error message on Ltac name clash with primitive tacticsGravatar xclerc2014-01-10
|
* Algebraized "No such hypothesis" errorsGravatar Pierre-Marie Pédrot2014-01-06
|
* Code cleaning in Rewrite, may also result faster.Gravatar Pierre-Marie Pédrot2014-01-04
|
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
| | | | | | To make this possible the state id has to reach the kernel. Hence definition_entry has an extra field, and many files had to be fixed.
* Simplifying the use of hypinfos in Rewrite.Gravatar Pierre-Marie Pédrot2013-12-24
|
* Rewrite.ml: removing direction flag from hypinfo.Gravatar Pierre-Marie Pédrot2013-12-23
|
* Do not pass unification flags around in Rewrite.Gravatar Pierre-Marie Pédrot2013-12-22
|
* Slight code cleaning ensuring more static invariants in Rewrite.Gravatar Pierre-Marie Pédrot2013-12-22
|
* Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atGravatar Pierre-Marie Pédrot2013-12-22
| | | | internalization time.
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
|
* Using interp_genarg in tactic notations where possible, instead of an ad-hocGravatar Pierre-Marie Pédrot2013-12-19
| | | | interpreter.
* Bad use of Obj.magic in interpretation of TacAlias arguments.Gravatar Pierre Boutillier2013-12-19
| | | | | | It triggered nonsensical behaviour of list-using tactic notation. Hopefully or not, nobody uses such notations out of the test-suite...
* Printing function for Stdargs in debuggerGravatar Pierre Boutillier2013-12-19
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-16 09:07:21 +0000