| Commit message (Expand) | Author | Age |
* | kernel/declarations becomes a pure mli | letouzey | 2013-02-26 |
* | Names: shortcuts for building {kn, constant, mind} with empty sections | letouzey | 2013-02-26 |
* | Names: Modularize constant and mutual_inductive | letouzey | 2013-02-26 |
* | Dir_path --> DirPath | letouzey | 2013-02-19 |
* | Classops : avoid some use of Gmap | letouzey | 2013-02-19 |
* | use List.rev_map whenever possible | letouzey | 2013-02-18 |
* | Minor code cleanups, especially take advantage of Dir_path.is_empty | letouzey | 2013-02-18 |
* | Extraction: same as commit 16203, hopefully without NotASort exns | letouzey | 2013-02-18 |
* | Fix extraction of inductive types that Coq auto-detects to be in Prop | letouzey | 2013-02-14 |
* | No reason a priori for using unfiltered env for printing | herbelin | 2013-01-29 |
* | Fixed synchronicity of filter with evar context in new_goal_with. | herbelin | 2013-01-29 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |
* | Unset Asymmetric Patterns | pboutill | 2013-01-18 |
* | Array.create is deprecated | pboutill | 2012-12-19 |
* | Modulification of name | ppedrot | 2012-12-18 |
* | Modulification of mod_bound_id | ppedrot | 2012-12-18 |
* | Modulification of Label | ppedrot | 2012-12-18 |
* | Extraction: qualified names in Extract Constant examples (fix #2878) | letouzey | 2012-12-18 |
* | No more constant named "int" in Coq theories (cf bug #2878) | letouzey | 2012-12-18 |
* | Extraction of projections: restrict a hack to ocaml only (fix #2941) | letouzey | 2012-12-17 |
* | Modulification of dir_path | ppedrot | 2012-12-14 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Moved Stringset and Stringmap to String namespace. | ppedrot | 2012-12-14 |
* | Moved Intset and Intmap to Int namespace. | ppedrot | 2012-12-14 |
* | Ensure that a function declared with a label is used with it | letouzey | 2012-12-08 |
* | Taking into account the type of a definition (if it exists), and the | herbelin | 2012-11-17 |
* | More monomorphizations | ppedrot | 2012-11-13 |
* | Added a CString module. | ppedrot | 2012-11-13 |
* | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot | 2012-11-08 |
* | correcting a little bug in Function | jforest | 2012-10-31 |
* | Extraction Implicit: consider the parameters of a constructor (fix #2905) | letouzey | 2012-10-30 |
* | Extraction: avoid initial strange empty comments after Arnaud's hack | letouzey | 2012-10-30 |
* | Fix Separate extraction when a module-as-file is aliased (#2917) | letouzey | 2012-10-30 |
* | Change Hint Resolve, Immediate to take a global reference as argument | msozeau | 2012-10-26 |
* | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey | 2012-10-16 |
* | still some more dead code removal | letouzey | 2012-10-06 |
* | remove useless hidden_flag in TacMutual(Co)Fix | letouzey | 2012-10-06 |
* | remove dumptree.ml4 | letouzey | 2012-10-06 |
* | Clean-up : removal of Proof_type.tactic_expr | letouzey | 2012-10-06 |
* | Proof_type: rule now degenerates to prim_rule | letouzey | 2012-10-06 |
* | Clean-up : no more Proof_type.proof_tree | letouzey | 2012-10-06 |
* | Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box | letouzey | 2012-10-06 |
* | Moved Compat to parsing. This permits to break the dependency of the | ppedrot | 2012-10-04 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | Ltac repeat is in fact already doing progress | letouzey | 2012-10-01 |
* | Cleaning, renaming obscure functions and documenting in Hashcons. | ppedrot | 2012-09-26 |
* | Fixing a bug introduced in Funind plugin when reorganizing the CList | ppedrot | 2012-09-24 |
* | More cleaning in CArray... | ppedrot | 2012-09-18 |
* | More cleanup of Util: utf8 aspects moved to a new file unicode.ml | letouzey | 2012-09-18 |