aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Fixing pervasive equalities. In particular, I removed the code that deletedGravatar Pierre-Marie Pédrot2014-03-03
* 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
* 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
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* 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
* Tacinterp: refactoring using Monad.Gravatar Arnaud Spiwack2014-02-27
* 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
* Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Gravatar Arnaud Spiwack2014-02-27
* Get rid of the enterl/glist API for Proofview.Goal.Gravatar Arnaud Spiwack2014-02-27
* Tacinterp: yet another superfluous enterl.Gravatar Arnaud Spiwack2014-02-27
* Tacinterp: spurious enterl.Gravatar Arnaud Spiwack2014-02-27
* 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
* Tacinterp: fewer enterl still.Gravatar Arnaud Spiwack2014-02-25
* Tacinterp: fewer Proofview.Goal.enterl.Gravatar Arnaud Spiwack2014-02-25
* 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
* Removing non-marshallable data from the Agram constructor. Instead ofGravatar Pierre-Marie Pédrot2014-02-16
* 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
* Fixing dependent inversion. Some exceptions were not caught by the tacticGravatar Pierre-Marie Pédrot2014-01-28
* 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 hyp...Gravatar Pierre-Marie Pédrot2014-01-17
* 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
* 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
* 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
* Bad use of Obj.magic in interpretation of TacAlias arguments.Gravatar Pierre Boutillier2013-12-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 17:36:19 +0000