| Age | Commit message (Expand) | Author |
|---|
| 2013-06-22 | Now, idtac closures use maps instead of association list. | ppedrot |
| 2013-06-22 | Generalizing the use of maps instead of lists in the interpretation | ppedrot |
| 2013-06-21 | Splitted up Genarg in four different levels: | ppedrot |
| 2013-06-21 | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot |
| 2013-06-21 | Revert "parse "of" as KEYID "of"" | gareuselesinge |
| 2013-06-19 | parse "of" as KEYID "of" | gareuselesinge |
| 2013-06-18 | Removing the various glob/subst/interp registering functions for | ppedrot |
| 2013-06-10 | Hiding tactic value representations. | ppedrot |
| 2013-06-06 | Uniformizing generic argument types. | ppedrot |
| 2013-06-05 | Replacing lists by maps in matching interpretation. | ppedrot |
| 2013-05-30 | bwaa, a Pervasive.compare | pboutill |
| 2013-05-29 | newring.ml4: interp constr arg at interp time (not parse time) | gareuselesinge |
| 2013-05-12 | Removing Gmap from Extraction plugin | ppedrot |
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-05-09 | Use definition_entry to declare local definitions | gareuselesinge |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2013-05-08 | Uniformizing the [if_warn] flag used for warning printing and put | ppedrot |
| 2013-05-06 | States: frozen states can hold closures | gareuselesinge |
| 2013-05-05 | Little fix for Nsatz: hypotheses not directly relevant to the nsatz | herbelin |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-04-23 | Indfun : use States.with_state_protection instead of freeze/unfreeze | letouzey |
| 2013-04-22 | code simplifications concerning Summary | letouzey |
| 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 |
