aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
Commit message (Expand)AuthorAge
* Reductionops.Stack.strip* are ready to deal with ShiftGravatar Pierre Boutillier2014-02-24
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Optimization in unification: when checking that the head of a term is anGravatar ppedrot2013-10-29
* Useless array-to-list casts in Unification.Gravatar ppedrot2013-10-29
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
* - install evar printer for debuggingGravatar msozeau2013-10-29
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Small optimizations in unification.Gravatar ppedrot2013-10-23
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* - Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...Gravatar msozeau2013-07-19
* - Keep the refinement of existing evars comming from unification with a rewri...Gravatar msozeau2013-06-19
* Little oversight in commit r16489 (fix for bug #3036).Gravatar herbelin2013-05-10
* Protection against "Bad recursive type" in w_unify0 (bug #3036).Gravatar herbelin2013-05-08
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Fix bug #2989: make unification.ml able to deal with canonical structure in a...Gravatar pboutill2013-03-25
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...Gravatar pboutill2013-02-25
* A more informative message when the elimination predicate forGravatar herbelin2013-02-17
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Splitted Evarutil in two filesGravatar ppedrot2013-02-10
* Revert "Ordered evars by level of dependency in the merging phase of unificat...Gravatar herbelin2013-02-05
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Ordered evars by level of dependency in the merging phase of unificationGravatar herbelin2013-01-27
* Fixed a little inefficiency of "set/destruct" over a pattern. NowGravatar herbelin2012-12-18
* Factorization of the elim unif flag with the default flag. SinceGravatar herbelin2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
* Improving error message when abtraction over goal (abstract_list_allGravatar herbelin2012-10-04
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Unification in Evar_conv uses an abstract machine stateGravatar pboutill2012-08-09
* Updating headers.Gravatar herbelin2012-08-08
* Reductionops refactoringGravatar pboutill2012-07-20
* Continuing r15459: it helps testing occur-check early in someGravatar herbelin2012-07-06
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Fixing bug #2817 (occur check was not done up to instantiation ofGravatar herbelin2012-06-20
* Reductionops : Better abstract machine stack utilitiesGravatar pboutill2012-06-15
* Forward-port fixes from 8.4 (15358, 15353, 15333).Gravatar msozeau2012-06-04
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Remove support for "abstract typing constraints" that requires unicity of sol...Gravatar msozeau2012-03-14