aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.mli
AgeCommit message (Expand)Author
2014-10-01Fix cbn behavior wrt simpl no matchPierre Boutillier
2014-10-01Fix the refolding by cbn of mutal constants defined in not included modulesPierre Boutillier
2014-09-29In evarconv and unification, expand folded primitive projections toMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-06-13Adapt simpl/cbn unfolding and refolding machinery to projections, so thatMatthieu Sozeau
2014-06-11- Fix bug #3368, due to wrong use of the Cst_stack for projections.Matthieu Sozeau
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-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-28Dead code elimionation in reductionopsPierre Boutillier
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre 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-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-10-29Do not generate useless argument arrays in whd_* functions.ppedrot
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-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-01-24Reductionops: whd_state_gen can take and answers a cst_stack toopboutill
2012-12-21Awful heuristic to refold mutual fixpoint in reductionopspboutill
2012-12-19Reductionops reduction machine can refold constantpboutill
2012-12-18Modulification of nameppedrot
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
2012-08-08Updating headers.herbelin
2012-07-20Reductionops refactoringpboutill
2012-07-12tacred uses stack_reduction_function instead of state_reduction_functionpboutill
2012-06-15Reductionops abstract machine uses Zcase & Zfix stack node.pboutill
2012-06-15Reductionops : Better abstract machine stack utilitiespboutill
2012-01-31Bug #2041: unfold at betaiotaZETA normalize like unfoldpboutill
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
2011-06-19Ensured that the transparency state is used when flag betaiota is on for apply.herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-12-21Generic support for open terms in tacticsherbelin
2009-12-14Improved strategy for rewriting lemma possibly depending because of evars.herbelin
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:37:27 +0000