| Age | Commit message (Expand) | Author |
|---|
| 2013-08-25 | Removing association lists in Reductionops. Btw, defining the dual of the | ppedrot |
| 2013-07-19 | - Fix uncaught exception NotASort from reductionops, moving decomp_sort to re... | msozeau |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-25 | Fix bug #2989: make unification.ml able to deal with canonical structure in a... | pboutill |
| 2013-03-23 | Minor code cleaning in CArray / CList. | ppedrot |
| 2013-03-14 | Typo in an error message | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 7) | letouzey |
| 2013-03-05 | More monomorphization. | ppedrot |
| 2013-02-28 | compare_stack_shape before ise_stack2 in evar_conv | pboutill |
| 2013-02-25 | Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo... | pboutill |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-28 | Added backtrace information to anomalies | ppedrot |
| 2013-01-24 | Reductionops: whd_state_gen can take and answers a cst_stack too | pboutill |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-21 | Awful heuristic to refold mutual fixpoint in reductionops | pboutill |
| 2012-12-21 | Fixup and comment reductionops | pboutill |
| 2012-12-19 | Reductionops reduction machine can refold constant | pboutill |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-28 | Reductionops uses Closure.reds | pboutill |
| 2012-11-22 | Monomorphization (pretyping) | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | This patch removes unused "open" (automatically generated from | regisgia |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-25 | Fix eta contraction in Reductionops | pboutill |
| 2012-07-20 | Reductionops refactoring | pboutill |
| 2012-07-12 | tacred uses stack_reduction_function instead of state_reduction_function | pboutill |
| 2012-06-15 | Reductionops abstract machine uses Zcase & Zfix stack node. | pboutill |
| 2012-06-15 | Reductionops : Better abstract machine stack utilities | pboutill |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-01-31 | Bug #2041: unfold at betaiotaZETA normalize like unfold | pboutill |
| 2011-10-05 | It happens that the type inference algorithm (pretyping) did not check | herbelin |
| 2011-08-10 | Propagated information from the reduction tactics to the kernel so | herbelin |
| 2011-06-19 | Ensured that the transparency state is used when flag betaiota is on for apply. | herbelin |
| 2011-02-17 | - Use transparency information all the way through unification and | msozeau |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-07-29 | kernel conversion and reduction do not raise assert failure on ill-typed term... | barras |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-12 | Fixed bug #2135 (second-order unification was raising cryptic message) | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-12-21 | Generic support for open terms in tactics | herbelin |
| 2009-12-14 | Improved strategy for rewriting lemma possibly depending because of evars. | herbelin |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-06-02 | Adding a regression test about Bauer's example on coq-club of | herbelin |
| 2009-05-27 | Populate the sort constraints set correctly during unification. Add a | msozeau |
| 2009-04-08 | - Fixing bug #2084 (unification not checking sort constraints), hoping | herbelin |
