| Age | Commit message (Expand) | Author |
|---|
| 2013-04-15 | Checker: regroup all vo-related types in cic.mli | letouzey |
| 2013-03-25 | Comments in mli | pboutill |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 5) | letouzey |
| 2013-03-12 | Term.dest* functions now raise specific DestKO exn instead of Invalid_argument | letouzey |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-11-26 | Removed some FIXME related to equality on universes. | ppedrot |
| 2012-11-13 | More monomorphizations | ppedrot |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-20 | Fixing bug #2817 (occur check was not done up to instantiation of | herbelin |
| 2012-03-20 | Reorganizing the structure of evarutil.ml (only restructuration, no | herbelin |
| 2012-03-13 | Fixing vm_compute bug #2729 (function used to decompose constructors | herbelin |
| 2011-10-11 | More on r14536 (an unused pattern-matching remained in the commit). | herbelin |
| 2011-10-10 | Hash-consing of mutual_inductive_body (and Univ.constraints) | letouzey |
| 2011-10-02 | Hash-consing of constr could share more | letouzey |
| 2011-09-22 | Remove specific hash-consing of Term.types (was unused anyway) | letouzey |
| 2011-09-08 | More twicks on hash-consing | letouzey |
| 2011-08-10 | Propagated information from the reduction tactics to the kernel so | herbelin |
| 2011-07-29 | Extraction: replace generic = on mutual_inductive_body by mib_equal | puech |
| 2011-07-29 | Term: moved function constr_ord (a.k.a compare_constr) from Sequent to Term | puech |
| 2011-07-29 | Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons... | puech |
| 2011-07-29 | Term: added function eq_named_declaration | puech |
| 2011-04-06 | A few extra combinators about rel_declaration/named_declaration + a bit of doc | herbelin |
| 2010-12-19 | Fixing bug #2454: inversion predicate strategy for inferring the type | herbelin |
| 2010-11-03 | Remove suspiciously named "implicit" stuff from Term | glondu |
| 2010-10-05 | Reintroduce kind_of_type (used by Presburger contrib) | glondu |
| 2010-09-28 | Remove kind_of_type, kind_of_term2 (dead code) | glondu |
| 2010-09-24 | Partial review of removed dead code (r13460) | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-22 | New script dev/tools/change-header to automatically update Coq files headers. | herbelin |
| 2010-04-29 | "make source-doc" builds documentation of mli in html and pdf at | pboutill |
| 2010-04-29 | Various minor improvements of comments in mli for ocamldoc | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-03-12 | fixed confusion between number of cstr arguments and number of pattern variab... | barras |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-08-11 | Ensures that let-in's in arities of inductive types work well. Maybe not | herbelin |
| 2009-05-18 | Minor unification changes: | msozeau |
| 2008-12-31 | Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod -> | herbelin |
| 2008-10-18 | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-04-27 | Correction du bug des types singletons pas sous-type de Set | herbelin |
| 2008-03-28 | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau |
| 2008-03-09 | Fix a few bugs in Program: use user-given typing constraints for | msozeau |
| 2008-01-31 | Finish let| implementation and document it | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-18 | Nettoyage de code en vue de la release. Plus de Warning: Unused | aspiwack |
