aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-03-30Added take to VectorDef.George Stelle
2017-03-30Merge PR#511: [stm] Remove some obsolete vernacs/classification.Maxime Dénès
2017-03-29Merge PR#522: [coqide] Protect against size_allocate race in proofview.Maxime Dénès
2017-03-29Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-29Merge PR#514: [travis] Backport from trunk: VSTMaxime Dénès
2017-03-29Merge PR#506: [nit] Fix a couple incorrect uses of msg_error.Maxime Dénès
2017-03-29Merge PR#521: Do so that "About" tells if a reference is a coercion.Maxime Dénès
2017-03-29Merge PR#525: [ide] Fix typo in pp serialization.Maxime Dénès
2017-03-29Merge branch 'trunk' into pr379Maxime Dénès
2017-03-29Fix call to broken unsafe_type_of in apply tactic.Maxime Dénès
2017-03-29Run non-tactic comands without resilient_commandTej Chajed
2017-03-29[ide] Fix typo in pp serialization.Emilio Jesus Gallego Arias
2017-03-28Revert to incorrect heuristic in apply.Maxime Dénès
2017-03-28Fixing missing PropFacts.v in Logic/vo.itarget.Hugo Herbelin
2017-03-28[readme] Add badges for Travis and Gitter.Emilio Jesus Gallego Arias
2017-03-28[coqide] Protect against size_allocate race in proofview.Emilio Jesus Gallego Arias
2017-03-27Do so that "About" tells if a reference is a coercion.Hugo Herbelin
2017-03-27More efficient check in validity of side-effects.Pierre-Marie Pédrot
2017-03-27Adding the size of the opaquetab in its representation.Pierre-Marie Pédrot
2017-03-27Fix hashconsing of terms in the kernel.Pierre-Marie Pédrot
2017-03-25Mathcomp overlay.Maxime Dénès
2017-03-24Fix interpretation of Ltac patterns episode 2.Maxime Dénès
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24[travis] Backport from trunk: VSTEmilio Jesus Gallego Arias
2017-03-24Merge PR#489: [travis] Add VSTMaxime Dénès
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
2017-03-24[nit] Fix a couple incorrect uses of msg_error.Emilio Jesus Gallego Arias
2017-03-24[travis] Add VSTEmilio Jesus Gallego Arias
2017-03-24Applying same convention as in Definition for printing type in a let in.Hugo Herbelin
2017-03-24Applying same convention as in Definition for parsing type in a let in.Hugo Herbelin
2017-03-24Documenting main changes of API.Hugo Herbelin
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-03-24Using the same type of binders for interning and externing.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 13:17:59 +0000