aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.ml
AgeCommit message (Expand)Author
2014-06-04cbn understand ! Arguments directivePierre Boutillier
2014-05-26Cbn reduces Pos.compare p~1 q~1 to Pos.compare p qPierre Boutillier
2014-05-26Reduction.Stack.Fix/Case stores Cst_stack.tPierre Boutillier
2014-05-26Cst_stack before stack (abstraction leak in whd_gen)Pierre Boutillier
2014-05-26cbn: args list instead of arg numberPierre Boutillier
2014-05-26Reductionops.Stack.map & Reduction.iterate_whd_genPierre
2014-05-06- Fixes for canonical structure resolution (check that the initial term indee...Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
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-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-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
2013-11-08Removing partial applications in Reductionops.ppedrot
2013-11-05Preventing useless allocations in Reductionops.instance.ppedrot
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-10-29Do not generate useless argument arrays in whd_* functions.ppedrot
2013-10-29[Reductionops.append_stack_app]: do not allocate a useless array.ppedrot
2013-10-22Various optimizations in Constr, such as term sharing and allocationppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-08-25Removing association lists in Reductionops. Btw, defining the dual of theppedrot
2013-07-19- Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...msozeau
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-25Fix bug #2989: make unification.ml able to deal with canonical structure in a...pboutill
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-14Typo in an error messageletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 7)letouzey
2013-03-05More monomorphization.ppedrot
2013-02-28compare_stack_shape before ise_stack2 in evar_convpboutill
2013-02-25Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...pboutill
2013-02-19Dir_path --> DirPathletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-28Added backtrace information to anomaliesppedrot
2013-01-24Reductionops: whd_state_gen can take and answers a cst_stack toopboutill
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-21Awful heuristic to refold mutual fixpoint in reductionopspboutill
2012-12-21Fixup and comment reductionopspboutill
2012-12-19Reductionops reduction machine can refold constantpboutill
2012-12-14Modulification of identifierppedrot
2012-11-28Reductionops uses Closure.redspboutill
2012-11-22Monomorphization (pretyping)ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-03 05:48:33 +0000