aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-25Removing useless evar-related stuff.ppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-18Removing the last global evar generation in Term_dnet. The veryppedrot
2013-09-18Removing unused code from Term_dnet.ppedrot
2013-09-18Removing almost all new_untyped_evar, and a bunch of Evd.add.ppedrot
2013-09-18Taming the simpl evar hack that used to use negative evars.ppedrot
2013-09-12Unplugging Autoinstance. The code is still here if someone wishesppedrot
2013-09-05Optimizing some evar_maps manipulation. In particular, using a [map] insteadppedrot
2013-09-05Documentation of Evd.ppedrot
2013-09-05Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.ppedrot
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
2013-08-25Removing association lists in Reductionops. Btw, defining the dual of theppedrot
2013-08-25Actually using the domain function for maps.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-25Replacing lists by sets in clear tactic.ppedrot
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-08-22Misc changes around coqtop.ml :letouzey
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-04Removing useless casts between arrays and lists.ppedrot
2013-08-04Removing now useless merging primitives from Evd.ppedrot
2013-08-03Small fixes due to the arrival of OCaml 3.12.ppedrot
2013-08-01Fixing #3088. Translation from globconstrs to patterns was forgettingppedrot
2013-08-01Added printing of instance priority to the Print Instances command.ppedrot
2013-07-19- Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...msozeau
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
2013-06-24Using the whole tactic environment while Pretyping.ppedrot
2013-06-22Generalizing the use of maps instead of lists in the interpretationppedrot
2013-06-19- Keep the refinement of existing evars comming from unification with a rewri...msozeau
2013-06-12One more fix for rewrite: disallow resolving of the (partial) constraintsmsozeau
2013-06-05Replacing lists by maps in matching interpretation.ppedrot
2013-05-30Do not compute fallback eagerly in Evarconvpboutill
2013-05-30export Unification.abstract_list_all_with_dependenciespboutill
2013-05-30Why not going inside fixpoint definition with appcontext ?pboutill
2013-05-30comments in mlipboutill
2013-05-28Pushing lazy lists into Ltac. Now, the control flow is explicitppedrot
2013-05-24Code cleaning in Matching.ppedrot
2013-05-14Mini documentation (evar_absorb_arguments).herbelin
2013-05-14Delayed the computation of parameters in sort polymorphism ofherbelin
2013-05-14"change ... in ..." and "simpl ... in ..." now consider nestedherbelin
2013-05-14Fixing a regression in unification introduced in r16205 (error raisedherbelin
2013-05-14Removing Gmap from Classops. Fold order only mattered for printing.ppedrot
2013-05-14Removing useless uses of Gmap.ppedrot
2013-05-14Replacing compatibility layer for Fmap in Typeclasses. Code wasppedrot
2013-05-14More semantical-friendly function.ppedrot
2013-05-12Use the Hook module here and there.ppedrot
2013-05-11Fixing a source of evars leak, revealed by contrib QuicksortComplexityherbelin
2013-05-10Little oversight in commit r16489 (fix for bug #3036).herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 03:43:19 +0000