| Age | Commit message (Expand) | Author |
|---|
| 2013-04-15 | More functional implementation of locality_flag and program_mode | gareuselesinge |
| 2013-04-11 | Backport r16394 from 8.4: | msozeau |
| 2013-04-02 | Revised infrastructure for lazy loading of opaque proofs | letouzey |
| 2013-03-23 | Minor code cleaning in CArray / CList. | ppedrot |
| 2013-03-18 | Extraction AccessOpaque is now activated again by default (#2952) | letouzey |
| 2013-03-15 | Extract_env : correct exceptions mentionned in a try ... with | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 15) | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 11) | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 9) | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 7) | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 6) | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 5) | letouzey |
| 2013-03-12 | Recdef: an anomaly isn't so anomalous, occurs in 1618.v | letouzey |
| 2013-03-12 | Term.dest* functions now raise specific DestKO exn instead of Invalid_argument | letouzey |
| 2013-03-12 | invalid_arg instead of raise (Invalid_argement ...) | letouzey |
| 2013-03-12 | Allowing different types of, not to be mixed, generic Stores through | ppedrot |
| 2013-03-11 | Allowing (Co)Fixpoint to be defined local and Let-style. | ppedrot |
| 2013-03-11 | Added a Local Definition vernacular command. This type of definition | ppedrot |
| 2013-02-26 | 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-19 | Dir_path --> DirPath | letouzey |
| 2013-02-19 | Classops : avoid some use of Gmap | letouzey |
| 2013-02-18 | 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-14 | Fix extraction of inductive types that Coq auto-detects to be in Prop | letouzey |
| 2013-01-29 | 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-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2013-01-18 | Unset Asymmetric Patterns | pboutill |
| 2012-12-19 | Array.create is deprecated | pboutill |
| 2012-12-18 | 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-17 | Extraction of projections: restrict a hack to ocaml only (fix #2941) | letouzey |
| 2012-12-14 | 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-08 | Ensure that a function declared with a label is used with it | letouzey |
| 2012-11-17 | Taking into account the type of a definition (if it exists), and the | herbelin |
| 2012-11-13 | More monomorphizations | ppedrot |
| 2012-11-13 | Added a CString module. | ppedrot |
| 2012-11-08 | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot |
| 2012-10-31 | correcting a little bug in Function | jforest |
| 2012-10-30 | Extraction Implicit: consider the parameters of a constructor (fix #2905) | letouzey |
