aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2014-03-17Evarconv: exact_ise_stack looks to stack head before bodies or branchesPierre Boutillier
2014-03-16consider_remaining_unif_problems respects Conv_oraclePierre Boutillier
2014-03-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
2014-03-10Evarconv unification respects Conv_oraclePierre Boutillier
2014-03-10MaybeFlexible semantic changesPierre Boutillier
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Goptions do not rely anymore on generic equality.Pierre-Marie Pédrot
2014-03-02Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Pierre Letouzey
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-03-02Adding an equality function over glob_constrPierre-Marie Pédrot
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2014-03-01Fixing bad comparison in Detyping.Pierre-Marie Pédrot
2014-02-28Removing Pervasives.compare in Termdn.Pierre-Marie Pédrot
2014-02-28Removing a Pervasives.compare in Term_dnet.Pierre-Marie Pédrot
2014-02-28Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infini...Pierre Boutillier
2014-02-28Dead code elimionation in reductionopsPierre Boutillier
2014-02-27Tacinterp: refactoring using Monad.Arnaud Spiwack
2014-02-27Code refactoring thanks to the new Monad module.Arnaud Spiwack
2014-02-26remoteCounter: backup/restoreEnrico Tassi
2014-02-24IStream: change type of thunk, spare allocations.Arnaud Spiwack
2014-02-24Ensuring that the module Stack is opaque inside Reductionops.Pierre-Marie Pédrot
2014-02-24cbn understands ArgumentsPierre Boutillier
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre Boutillier
2014-02-24Create Debug Unification optionPierre Boutillier
2014-02-24No more translation array <-> list in Reductionops.StackPierre Boutillier
2014-02-24Reductionops.Stack.strip* are ready to deal with ShiftPierre Boutillier
2014-02-24Reductionops.Stack.app_node is secretPierre Boutillier
2014-02-24app_node, stack, state printersPierre Boutillier
2014-02-24Stack operations of Reductionops in Reductionops.StackPierre Boutillier
2014-02-12TC: honor the use_typeclasses flag in pretypingEnrico Tassi
2014-02-11Made Pre_env.lazy_val opaque.Pierre-Marie Pédrot
2014-02-03Tracking memory misallocation by trying to improve sharing.Pierre-Marie Pédrot
2014-01-29Using Map.smartmap whenever deemed useful.Pierre-Marie Pédrot
2014-01-27Abstracting away coercion indexes in Classops.Pierre-Marie Pédrot
2014-01-26Coercions: avoid imperative data structureEnrico Tassi
2014-01-07STM: additional fix for STM + vm_computeEnrico Tassi
2013-12-30When resetting an evarmap with the unsafe function Evd.evars_reset_evd withPierre-Marie Pédrot
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
2013-12-06Fix test-suite/success/evars.v.Arnaud Spiwack
2013-12-03Removing useless meta-related functions.Pierre-Marie Pédrot
2013-11-30Better heuristic for name generation backward compatibility. We fallbackPierre-Marie Pédrot
2013-11-30Useless instantiation function exported in Evd.Pierre-Marie Pédrot
2013-11-30Tentative fix to recover fresh name generation as it was beforePierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-25Factoring: is_section_variable.Arnaud Spiwack
2013-11-25Typo resulting in bad eta-expansion of destructing let's body.Hugo Herbelin
2013-11-14Update comments in matching.mli.aspiwack
2013-11-08Removing partial applications in Reductionops.ppedrot
2013-11-07Partial application hunt.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 08:56:52 +0000