aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.mli
Commit message (Expand)AuthorAge
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* 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
* 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
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Dead code elimionation in reductionopsGravatar Pierre Boutillier2014-02-28
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar 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
* 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
* 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
* compare_stack_shape before ise_stack2 in evar_convGravatar pboutill2013-02-28
* Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...Gravatar pboutill2013-02-25
* Reductionops: whd_state_gen can take and answers a cst_stack tooGravatar pboutill2013-01-24
* Awful heuristic to refold mutual fixpoint in reductionopsGravatar pboutill2012-12-21
* Reductionops reduction machine can refold constantGravatar pboutill2012-12-19
* Modulification of nameGravatar ppedrot2012-12-18
* Unification in Evar_conv uses an abstract machine stateGravatar pboutill2012-08-09
* Updating headers.Gravatar herbelin2012-08-08
* Reductionops refactoringGravatar pboutill2012-07-20
* tacred uses stack_reduction_function instead of state_reduction_functionGravatar pboutill2012-07-12
* Reductionops abstract machine uses Zcase & Zfix stack node.Gravatar pboutill2012-06-15
* Reductionops : Better abstract machine stack utilitiesGravatar pboutill2012-06-15
* Bug #2041: unfold at betaiotaZETA normalize like unfoldGravatar pboutill2012-01-31
* It happens that the type inference algorithm (pretyping) did not checkGravatar herbelin2011-10-05
* Ensured that the transparency state is used when flag betaiota is on for apply.Gravatar herbelin2011-06-19
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* Improved strategy for rewriting lemma possibly depending because of evars.Gravatar herbelin2009-12-14
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Backtrack sur la mémoïsation de nf_evar.Gravatar aspiwack2009-03-04
* =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...Gravatar aspiwack2009-02-27
* pushed evar reduction in kernelGravatar barras2009-02-06