aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-03-24Unifying standard "constr_level" names for constructors of local_binder_expr.Hugo Herbelin
2017-03-24Renaming local_binder into local_binder_expr.Hugo Herbelin
2017-03-24Merging glob_binder and glob_decl.Hugo Herbelin
2017-03-24Type extended_glob_local_binder now contains only glob_constr.Hugo Herbelin
2017-03-24Standardized the order of constructors for binders: Assum then Def.Hugo Herbelin
2017-03-24Cleaning phase around local binder at glob level:Hugo Herbelin
2017-03-24"Standardizing" the name LocalPatten into LocalRawPattern.Hugo Herbelin
2017-03-24Better algorithm for Evarconv.max_undefined_with_candidates.Pierre-Marie Pédrot
2017-03-24Merge PR#392: strengthened the statement of JMeq_eq_depMaxime Dénès
2017-03-24Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-24Merge PR#476: [future] Be eager when "chaining" already resolved future values.Maxime Dénès
2017-03-24Merge PR#475: Opaque side effectsMaxime Dénès
2017-03-24Merge PR#504: [META] add support for ide librariesMaxime Dénès
2017-03-23Documenting the grammar {| ... |} syntax for building records.Hugo Herbelin
2017-03-23Supporting arbitrary binders in record fields, including e.g. patterns.Hugo Herbelin
2017-03-23Removing a redundant line in the syntax of record fields.Hugo Herbelin
2017-03-23Factorizing/unifying code in dealing with binders.Hugo Herbelin
2017-03-23Improving the API of constrexpr_ops.mli.Hugo Herbelin
2017-03-23A test checking for non-collision of name in irrefutable patterns.Hugo Herbelin
2017-03-23Merge PR#503: make check not CoqIDE-specificMaxime Dénès
2017-03-23Correctly identify [Time Defined.] as a definedTej Chajed
2017-03-23Merge PR#433: doc: fix a French-ismMaxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#507: Intern names bound in match patternsMaxime Dénès
2017-03-23Documenting the API of side-effects.Pierre-Marie Pédrot
2017-03-23Using a dedicated datastructure for side effect ordering.Pierre-Marie Pédrot
2017-03-23Making the side_effects type opaque.Pierre-Marie Pédrot
2017-03-23Intern names bound in match patternsTej Chajed
2017-03-23Merge PR#501: [travis] Fix iris-coq build.Maxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk.Maxime Dénès
2017-03-23Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Maxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-23Merge PR#495: funind: Ignore missing info for current functionMaxime Dénès
2017-03-23Make the computation of frozen evars lazy in Pretyping.Pierre-Marie Pédrot
2017-03-23Fast path in computation of frozen evars in Pretyping.Pierre-Marie Pédrot
2017-03-23Fast path for implicit tactic solving.Pierre-Marie Pédrot
2017-03-23Ensuring static invariants about handling of pending evars in Pretyping.Pierre-Marie Pédrot
2017-03-23Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Maxime Dénès
2017-03-23Merge PR#491: Do not typecheck twice the type of opaque constants.Maxime Dénès
2017-03-23[META] add support for ide librariesEmilio Jesus Gallego Arias
2017-03-22Merge PR#480: show unused intro pattern warningMaxime Dénès
2017-03-22Merge PR#493: [safe-string] update dev/doc/changesMaxime Dénès
2017-03-22Merge PR#415: Use a compact representation for real literalsMaxime Dénès
2017-03-22make check not CoqIDE-specificPaul Steckler
2017-03-22[pp] Add anomaly header to anomaly error messages.Emilio Jesus Gallego Arias
2017-03-22Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.Hugo Herbelin
2017-03-22[travis] Fix iris-coq build.Emilio Jesus Gallego Arias
2017-03-22Document the changes to IZR.Guillaume Melquiond
2017-03-22Make IZR a morphism for field.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 08:07:43 +0000