aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Rewriting [lapply] tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-04-27
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Better representation of evar filters: we represent the vacuous filters ofGravatar Pierre-Marie Pédrot2014-04-23
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Removing tactic compatibility layer from Elim.Gravatar Pierre-Marie Pédrot2014-04-22
* Simplifying interface of elimination tactics. They used dummy clausenvs, andGravatar Pierre-Marie Pédrot2014-04-22
* Adding a [map] primitive to the tactic monad. Hopefully this should beGravatar Pierre-Marie Pédrot2014-04-20
* Transfering the initial goals from the proofview to the proof object.Gravatar Pierre-Marie Pédrot2014-04-07
* Removing unused functions in Refiner.Gravatar Pierre-Marie Pédrot2014-04-06
* Actually using the [modify] primitive.Gravatar Pierre-Marie Pédrot2014-04-06
* Adding an [modify] function to the tactic monad. It allows to modifyGravatar Pierre-Marie Pédrot2014-04-06
* Evars introduced by Proofview refining are flagged as GoalEvar. For someGravatar Pierre-Marie Pédrot2014-04-01
* Removing the Change_evar refiner rule.Gravatar Pierre-Marie Pédrot2014-03-31
* Lighter interface for creating refining tactics.Gravatar Pierre-Marie Pédrot2014-03-28
* Removing tactic compatibility layer from Eqdecide.Gravatar Pierre-Marie Pédrot2014-03-27
* Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing Tacmach compatibility layer in Inv.Gravatar Pierre-Marie Pédrot2014-03-26
* Moving some tactic code to the new engine.Gravatar Pierre-Marie Pédrot2014-03-26
* Using non-normalized goals in tactic interpretation.Gravatar Pierre-Marie Pédrot2014-03-19
* Adding phantom types to discriminate normalized goals, and adding a way toGravatar Pierre-Marie Pédrot2014-03-19
* Potentially unused computation in Goal.Gravatar Pierre-Marie Pédrot2014-03-07
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* 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
* 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
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Tacinterp: fewer Proofview.Goal.enterl.Gravatar Arnaud Spiwack2014-02-25
* cbn understands ArgumentsGravatar Pierre Boutillier2014-02-24
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* More sharing in Logic, together with some code cleaning.Gravatar Pierre-Marie Pédrot2014-02-21
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
* STM: fix valid_id coming from Qed errorsGravatar Enrico Tassi2014-02-10
* Tracking memory misallocation by trying to improve sharing.Gravatar Pierre-Marie Pédrot2014-02-03
* Fixing backtrace reporting.Gravatar Pierre-Marie Pédrot2014-02-02
* Typos in comment.Gravatar Arnaud Spiwack2014-01-31
* Fixing backtrace handling here and there.Gravatar Pierre-Marie Pédrot2014-01-30
* Useless Array.of_listGravatar Pierre-Marie Pédrot2014-01-10
* Exporting the full pretyper options in Goal.constr_of_raw.Gravatar Pierre-Marie Pédrot2014-01-10
* Algebraized "No such hypothesis" errorsGravatar Pierre-Marie Pédrot2014-01-06
* Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, wit...Gravatar Arnaud Spiwack2014-01-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 22:25:47 +0000