aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenvtac.ml
AgeCommit message (Expand)Author
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
2012-06-04Forward-port fixes from 8.4 (15358, 15353, 15333).msozeau
2012-03-20Fix interface of resolve_typeclasses: onlyargs -> with_goals:msozeau
2012-03-02Noise for nothingpboutill
2011-12-17Added a flag to control the use of typing when instantiating appliedherbelin
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
2011-06-13Added a flag to restrict conversion in tactic unification on theherbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 02:29:11 +0000