| Commit message (Expand) | Author | Age |
* | Now printing body of abbreviations (i.e. notation with a name) with | herbelin | 2013-05-05 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | Renaming SearchAbout into Search and Search into SearchHead. | herbelin | 2013-04-17 |
* | Improving error message in explain_cannot_find_well_typed_abstraction: | herbelin | 2013-04-17 |
* | More functional implementation of locality_flag and program_mode | gareuselesinge | 2013-04-15 |
* | Revised infrastructure for lazy loading of opaque proofs | letouzey | 2013-04-02 |
* | Minor code cleaning in CArray / CList. | ppedrot | 2013-03-23 |
* | Robust display of NotConvertibleTypeField errors (fix #3008, #2995) | letouzey | 2013-03-21 |
* | Printmod: handle more examples thanks to better nametab use | letouzey | 2013-03-21 |
* | Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983) | letouzey | 2013-03-21 |
* | Ppvernac: no globalization for printing ltac definitions | letouzey | 2013-03-17 |
* | Pptactic.pr_raw_tactic is now without env argument | letouzey | 2013-03-14 |
* | Modules and ppvernac, sequel of Enrico's commit 16261 | letouzey | 2013-03-13 |
* | Declaremods: a few syntactic improvements | letouzey | 2013-03-13 |
* | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey | 2013-03-13 |
* | Restrict (try...with...) to avoid catching critical exn (part 5) | letouzey | 2013-03-13 |
* | 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-03-11 |
* | Use with_state_protection in pr_module_vardecls | gareuselesinge | 2013-03-08 |
* | More monomorphization. | ppedrot | 2013-03-05 |
* | kernel/declarations becomes a pure mli | letouzey | 2013-02-26 |
* | Names: shortcuts for building {kn, constant, mind} with empty sections | letouzey | 2013-02-26 |
* | Dir_path --> DirPath | letouzey | 2013-02-19 |
* | Removing Exc_located and using the new exception enrichement | ppedrot | 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 |
* | Added propagation of evars unification failure reasons for better | herbelin | 2013-02-17 |
* | Useless use of hooks in VernacDefinition. In addition, this was | ppedrot | 2013-02-10 |
* | No reason a priori for using unfiltered env for printing | herbelin | 2013-01-29 |
* | Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env | herbelin | 2013-01-29 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | Avoid failure in debugger when printing Ltac names. | herbelin | 2013-01-27 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |
* | Yet a new reduction tactic in Coq : cbn | pboutill | 2012-12-21 |
* | Modulification of name | ppedrot | 2012-12-18 |
* | Modulification of mod_bound_id | ppedrot | 2012-12-18 |
* | Modulification of Label | ppedrot | 2012-12-18 |
* | 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 |
* | Print univ constraints generated by a constant or inductive (when flag is set) | barras | 2012-11-21 |
* | Cleaning and small optimization in CList. | ppedrot | 2012-11-20 |
* | Added a CString module. | ppedrot | 2012-11-13 |
* | Monomorphized a lot of equalities over OCaml integers, thanks to | ppedrot | 2012-11-08 |
* | Change [Hints Resolve] to still accept constrs as arguments | msozeau | 2012-10-31 |
* | Fixed #2926: | ppedrot | 2012-10-29 |
* | 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 |