aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-02-08Add overlay for EquationsMatthieu Sozeau
2019-02-08Fix issue found in GeoCoqMatthieu Sozeau
2019-02-08Add overlays for unicoq and mtac2Matthieu Sozeau
2019-02-08Add back the deprecated conv/cumul functions.Matthieu Sozeau
2019-02-08Document the unify_flags more throroughly in evarsolve.Matthieu Sozeau
2019-02-08[evarconv] Handle frozen evars in solve_unif_constraints_with_heuristicsMatthieu Sozeau
2019-02-08[evarconv] Clean second order matching of evdrefsMatthieu Sozeau
2019-02-08Change interfaces of evarconv as suggested by Enrico.Matthieu Sozeau
2019-02-08print_constr_env moved to Internal moduleMatthieu Sozeau
2019-02-08Fix warning unused variableMatthieu Sozeau
2019-02-08[occur_rigidly] Try improving occur-check approximationMatthieu Sozeau
2019-02-08Add an helper [instantiate_evar] functionMatthieu Sozeau
2019-02-08Flags of evar_conv_x/unifiers: rationalizeMatthieu Sozeau
2019-02-08Rename types_or_terms and the unification function typesMatthieu Sozeau
2019-02-08Fix indentation (removing tabs)Matthieu Sozeau
2019-02-08Correct occur_rigidlyMatthieu Sozeau
2019-02-08Abstraction namingMatthieu Sozeau
2019-02-08unification: abstract_list_all_with_dependencies fixMatthieu Sozeau
2019-02-08evarconv/evarsolve: HO matching algorithm with occurrence selectionMatthieu Sozeau
2019-02-08[evarconv] New flag handling for unifierMatthieu Sozeau
2019-02-08[stm] Filter some more arguments that shouldn't be sent to workers.Emilio Jesus Gallego Arias
2019-02-08locus: Add an AtLeastOneOccurrence constructor.Matthieu Sozeau
2019-02-08Evd/evarsolve: add an abstraction field to evars for unificationMatthieu Sozeau
2019-02-08Merge PR #9410: Make `Program` a regular attributeMatthieu Sozeau
2019-02-08Merge PR #9515: [Gitlab-CI] Automatic deployment of the standard library docu...Emilio Jesus Gallego Arias
2019-02-08Use math mode more.Tanaka Akira
2019-02-08Fix index of arguments of constructor in fixpoint.Tanaka Akira
2019-02-08Change parameters p_1...p_r to q_1...q_r.Tanaka Akira
2019-02-08Change the index "p" to "s" in "type of branches".Tanaka Akira
2019-02-08Change c to c' forgotten at exchanging c and c'.Tanaka Akira
2019-02-08Remove spaces just before period (non-math mode).Tanaka Akira
2019-02-08Remove spaces just before comma (non-math mode).Tanaka Akira
2019-02-08Remove "'" accidentaly added.Tanaka Akira
2019-02-08[Gitlab-CI] Automatic deployment of the standard library documentation to GH-...Vincent Laporte
2019-02-08Add item in release-process.md to ease upcoming releases of Coq in Docker HubErik Martin-Dorel
2019-02-07Merge PR #9499: [Gitlab-CI] Never attempt to build cachixThéo Zimmermann
2019-02-07Merge PR #9477: Makefiles: Fixes for byte compilationEnrico Tassi
2019-02-07Remove some non tailrec List.map from CList implementationsGaëtan Gilbert
2019-02-07Merge PR #9475: Automatic deployment of the user manual to GH-PagesGaëtan Gilbert
2019-02-07Add print_pure_econstr signatureThierry Martinez
2019-02-07Remove nondeterministic testsGaëtan Gilbert
2019-02-07[Gitlab-CI] Never attempt to build cachixVincent Laporte
2019-02-07Merge PR #9496: Avoid eqn when generating name in induction_gen.Pierre-Marie Pédrot
2019-02-07Merge PR #9498: [dune] Fix OCaml trunk build.Gaëtan Gilbert
2019-02-07Merge PR #9479: Remove the Plexing.Error exception.Emilio Jesus Gallego Arias
2019-02-07[dune] Fix OCaml trunk build.Emilio Jesus Gallego Arias
2019-02-06[Gitlab-CI] Deploy manual to GH-PagesVincent Laporte
2019-02-06Avoid eqn when generating name in induction_gen.Jasper Hugunin
2019-02-06Merge PR #9124: Document the possibility of declaring a Ltac name_goal.Clément Pit-Claudel
2019-02-06Merge PR #9456: The lowest universe level is 1.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 20:56:07 +0000