aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.ml
Commit message (Expand)AuthorAge
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Cleanup code for looking up projection bodies.Gravatar Matthieu Sozeau2014-09-06
* Debug RAKAMGravatar Pierre Boutillier2014-08-26
* Grammar: "avoiding to" isn't proper, eitherGravatar Jason Gross2014-08-25
* Fix bug introduced by earlier commit on first-order unification of primitiveGravatar Matthieu Sozeau2014-08-10
* - Fix handling of opaque polymorphic definitions which were turned transparent.Gravatar Matthieu Sozeau2014-08-03
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Rework code for refolding projections in whd_state/whd_simpl to allow ArgumentsGravatar Matthieu Sozeau2014-07-29
* Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).Gravatar Matthieu Sozeau2014-07-10
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Adapt simpl/cbn unfolding and refolding machinery to projections, so thatGravatar Matthieu Sozeau2014-06-13
* - Fix bug #3368, due to wrong use of the Cst_stack for projections.Gravatar Matthieu Sozeau2014-06-11
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* - Keep all <= constraints during refinement, otherwise we might miss collapse...Gravatar Matthieu Sozeau2014-06-04
* cbn understand ! Arguments directiveGravatar Pierre Boutillier2014-06-04
* Cbn reduces Pos.compare p~1 q~1 to Pos.compare p qGravatar Pierre Boutillier2014-05-26
* Reduction.Stack.Fix/Case stores Cst_stack.tGravatar Pierre Boutillier2014-05-26
* Cst_stack before stack (abstraction leak in whd_gen)Gravatar Pierre Boutillier2014-05-26
* cbn: args list instead of arg numberGravatar Pierre Boutillier2014-05-26
* Reductionops.Stack.map & Reduction.iterate_whd_genGravatar Pierre2014-05-26
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infini...Gravatar Pierre Boutillier2014-02-28
* Dead code elimionation in reductionopsGravatar Pierre Boutillier2014-02-28
* Ensuring that the module Stack is opaque inside Reductionops.Gravatar Pierre-Marie Pédrot2014-02-24
* cbn understands ArgumentsGravatar Pierre Boutillier2014-02-24
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar Pierre Boutillier2014-02-24
* No more translation array <-> list in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* Reductionops.Stack.strip* are ready to deal with ShiftGravatar Pierre Boutillier2014-02-24
* Reductionops.Stack.app_node is secretGravatar Pierre Boutillier2014-02-24
* app_node, stack, state printersGravatar Pierre Boutillier2014-02-24
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* Removing partial applications in Reductionops.Gravatar ppedrot2013-11-08
* Preventing useless allocations in Reductionops.instance.Gravatar ppedrot2013-11-05
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
* [Reductionops.append_stack_app]: do not allocate a useless array.Gravatar ppedrot2013-10-29
* Various optimizations in Constr, such as term sharing and allocationGravatar ppedrot2013-10-22
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Removing association lists in Reductionops. Btw, defining the dual of theGravatar ppedrot2013-08-25
* - Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...Gravatar msozeau2013-07-19
* 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
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
* Typo in an error messageGravatar letouzey2013-03-14
* Restrict (try...with...) to avoid catching critical exn (part 7)Gravatar letouzey2013-03-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 03:22:03 +0000