| Commit message (Expand) | Author | Age |
* | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin | 2014-10-20 |
* | Simplify evarconv thanks to new delta status of projections, | Matthieu Sozeau | 2014-09-30 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to | Hugo Herbelin | 2014-04-28 |
* | Fix typo in comment. | Maxime Dénès | 2014-03-05 |
* | Do not generate useless argument arrays in whd_* functions. | ppedrot | 2013-10-29 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | Checker: regroup all vo-related types in cic.mli | letouzey | 2013-04-15 |
* | Comments in mli | pboutill | 2013-03-25 |
* | Restrict (try...with...) to avoid catching critical exn (part 5) | letouzey | 2013-03-13 |
* | Term.dest* functions now raise specific DestKO exn instead of Invalid_argument | letouzey | 2013-03-12 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |
* | Modulification of name | ppedrot | 2012-12-18 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Removed some FIXME related to equality on universes. | ppedrot | 2012-11-26 |
* | More monomorphizations | ppedrot | 2012-11-13 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Fixing bug #2817 (occur check was not done up to instantiation of | herbelin | 2012-06-20 |
* | Reorganizing the structure of evarutil.ml (only restructuration, no | herbelin | 2012-03-20 |
* | Fixing vm_compute bug #2729 (function used to decompose constructors | herbelin | 2012-03-13 |
* | More on r14536 (an unused pattern-matching remained in the commit). | herbelin | 2011-10-11 |
* | Hash-consing of mutual_inductive_body (and Univ.constraints) | letouzey | 2011-10-10 |
* | Hash-consing of constr could share more | letouzey | 2011-10-02 |
* | Remove specific hash-consing of Term.types (was unused anyway) | letouzey | 2011-09-22 |
* | More twicks on hash-consing | letouzey | 2011-09-08 |
* | Propagated information from the reduction tactics to the kernel so | herbelin | 2011-08-10 |
* | 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-07-29 |
* | A few extra combinators about rel_declaration/named_declaration + a bit of doc | herbelin | 2011-04-06 |
* | Fixing bug #2454: inversion predicate strategy for inferring the type | herbelin | 2010-12-19 |
* | Remove suspiciously named "implicit" stuff from Term | glondu | 2010-11-03 |
* | Reintroduce kind_of_type (used by Presburger contrib) | glondu | 2010-10-05 |
* | Remove kind_of_type, kind_of_term2 (dead code) | glondu | 2010-09-28 |
* | Partial review of removed dead code (r13460) | herbelin | 2010-09-24 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | New script dev/tools/change-header to automatically update Coq files headers. | herbelin | 2010-06-22 |
* | "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-29 |
* | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |
* | fixed confusion between number of cstr arguments and number of pattern variab... | barras | 2010-03-12 |
* | This big commit addresses two problems: | soubiran | 2009-10-21 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Ensures that let-in's in arities of inductive types work well. Maybe not | herbelin | 2009-08-11 |
* | Minor unification changes: | msozeau | 2009-05-18 |