index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
Commit message (
Expand
)
Author
Age
...
*
Added Genarg as generic argument type.
ppedrot
2013-06-12
*
Uniformizing generic argument types.
ppedrot
2013-06-06
*
Removing useless uses of Gmap.
ppedrot
2013-05-14
*
Use the Hook module here and there.
ppedrot
2013-05-12
*
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
[prev]
[next]