aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenvtac.ml
Commit message (Expand)AuthorAge
* Fast path in Clenvtac.clenv_refine typeclass resolution.Gravatar Pierre-Marie Pédrot2016-09-09
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Prevent a useless evar normalization in Clenvtac.unify.Gravatar Pierre-Marie Pédrot2016-06-20
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Proofview.Goal.sigma returns an indexed evarmap.Gravatar Pierre-Marie Pédrot2015-10-20
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
* | Removing uselessly duplicated function in Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|/
* Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Gravatar Pierre-Marie Pédrot2015-05-18
* Update headers.Gravatar Maxime Dénès2015-01-12
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Add support for deactivating type class inference from induction/destruct.Gravatar Hugo Herbelin2014-10-13
* Revert "While resolving typeclass evars in clenv, touch only the ones that ap...Gravatar Matthieu Sozeau2014-09-17
* While resolving typeclass evars in clenv, touch only the ones that appear in theGravatar Matthieu Sozeau2014-09-17
* While we don't have a clean alternative to Clenvtac, add a primitiveGravatar Matthieu Sozeau2014-09-12
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Putting implicit arguments of Clenv.res_pf right.Gravatar Pierre-Marie Pédrot2014-06-25
* Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itGravatar Pierre-Marie Pédrot2014-06-24
* Clenvtac.res_pf is in the new tactic monad.Gravatar Pierre-Marie Pédrot2014-06-24
* Clenvtac.unify is in the new monad.Gravatar Pierre-Marie Pédrot2014-06-23
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Simplifying interface of elimination tactics. They used dummy clausenvs, andGravatar Pierre-Marie Pédrot2014-04-22
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Tachmach.New is now in Proofview.Goal.enter style.Gravatar aspiwack2013-11-02
* Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Backtrack on unneeded change of interface for pose_metas_as_evars.Gravatar msozeau2013-06-04
* Start documenting new [rewrite_strat] tactic that applies rewritingGravatar msozeau2013-06-04
* Finer fix for bug 3017, mark unresolvability only of goals that areGravatar msozeau2013-04-18
* Fix for bug #3017: wrong handling of the unresolvability statusGravatar msozeau2013-04-03
* Fixed a little inefficiency of "set/destruct" over a pattern. NowGravatar herbelin2012-12-18
* Monomorphization (proof)Gravatar ppedrot2012-11-25
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Forward-port fixes from 8.4 (15358, 15353, 15333).Gravatar msozeau2012-06-04
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Noise for nothingGravatar pboutill2012-03-02
* Added a flag to control the use of typing when instantiating appliedGravatar herbelin2011-12-17
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
* Added a flag to restrict conversion in tactic unification on theGravatar herbelin2011-06-13
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 15:26:27 +0000