aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenvtac.ml
AgeCommit message (Expand)Author
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-02-14Removing most nf_enter in tactics.Pierre-Marie Pédrot
2017-02-14Proofview.Goal primitive now return EConstrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Clenv API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-09-09Fast path in Clenvtac.clenv_refine typeclass resolution.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-20Prevent a useless evar normalization in Clenvtac.unify.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-20Proofview.Goal.sigma returns an indexed evarmap.Pierre-Marie Pédrot
2015-10-20Boxing the Goal.enter primitive into a record type.Pierre-Marie Pédrot
2015-09-27Removing uselessly duplicated function in Evd.Pierre-Marie Pédrot
2015-05-18Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-13Add support for deactivating type class inference from induction/destruct.Hugo Herbelin
2014-09-17Revert "While resolving typeclass evars in clenv, touch only the ones that ap...Matthieu Sozeau
2014-09-17While resolving typeclass evars in clenv, touch only the ones that appear in theMatthieu Sozeau
2014-09-12While we don't have a clean alternative to Clenvtac, add a primitiveMatthieu Sozeau
2014-09-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-06-25Putting implicit arguments of Clenv.res_pf right.Pierre-Marie Pédrot
2014-06-24Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itPierre-Marie Pédrot
2014-06-24Clenvtac.res_pf is in the new tactic monad.Pierre-Marie Pédrot
2014-06-23Clenvtac.unify is in the new monad.Pierre-Marie Pédrot
2014-05-06- Fixes for canonical structure resolution (check that the initial term indee...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-22Simplifying interface of elimination tactics. They used dummy clausenvs, andPierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
2013-11-02Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-08-08State Transaction Machinegareuselesinge
2013-06-04Backtrack on unneeded change of interface for pose_metas_as_evars.msozeau
2013-06-04Start documenting new [rewrite_strat] tactic that applies rewritingmsozeau
2013-04-18Finer fix for bug 3017, mark unresolvability only of goals that aremsozeau
2013-04-03Fix for bug #3017: wrong handling of the unresolvability statusmsozeau
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
2012-11-25Monomorphization (proof)ppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 14:54:06 +0000