aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-04-27Disambiguate Polynomial.Hyp and Mfourier.Hyp -> AssumGaetan Gilbert
2017-04-27Use [method!] to override methods (warning 7)Gaetan Gilbert
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-27Remove unused [rec] keywordsGaetan Gilbert
2017-04-27Locally disable some warnings.Gaetan Gilbert
2017-04-27Merge PR#414: Some more theory on powerRZ.Maxime Dénès
2017-04-27Merge PR#583: [toplevel] More work on error handling.Maxime Dénès
2017-04-27Merge PR#587: Fix description of command-line arguments for Add (Rec) LoadPathMaxime Dénès
2017-04-27fix order of command-line arguments mentioned in Add LoadPathPaul Steckler
2017-04-27Merge PR#586: trivial cleanup commits which does not change Coq APIMaxime Dénès
2017-04-27Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.Pierre-Marie Pédrot
2017-04-27Merge PR#568: Remove tactic compatibility layerMaxime Dénès
2017-04-27Tentative note in CHANGES about now applying βι while typing "match" branches.Hugo Herbelin
2017-04-27Test surgical use of beta-iota in the type of variables coming fromHugo Herbelin
2017-04-27A refined solution to the beta-iota discrepancies between 8.4 and 8.5 "refine".Hugo Herbelin
2017-04-27Document the API changes.Pierre-Marie Pédrot
2017-04-27Merge PR#584: Give andb_prop a simpler proofMaxime Dénès
2017-04-27Merge PR#585: Small typo in commentMaxime Dénès
2017-04-27Fast path when checking equality of universe levels in UState.Pierre-Marie Pédrot
2017-04-27Code cleaning in unification algorithm for universes.Pierre-Marie Pédrot
2017-04-27Merge branch 'v8.6'Pierre-Marie Pédrot
2017-04-27contracting the type of "Pfedit.solve_by_implicit_tactic"Matej Košík
2017-04-26Small typo in commentVadim Zaliva
2017-04-25transparent abstract: Respond to review commentJason Gross
2017-04-25transparent abstract: Respond to review commentJason Gross
2017-04-25Make opaque optional only for tclABSTRACTJason Gross
2017-04-25Generalize cache_term_by_tactic_thenJason Gross
2017-04-25Mark transparent_abstract as risky in docsJason Gross
2017-04-25Add transparent_abstract tacticJason Gross
2017-04-25Add support for transparent abstract (no syntax)Jason Gross
2017-04-25Give andb_prop a simpler proofJason Gross
2017-04-25[toplevel] Remove unused parameter from `Vernac.process_expr`.Emilio Jesus Gallego Arias
2017-04-25[toplevel] Use exception information for error printing.Emilio Jesus Gallego Arias
2017-04-25[located] [doc] Improve docs for `CAst.ast`.Emilio Jesus Gallego Arias
2017-04-25Fix an optimization failure in tclPROGRESS.Pierre-Marie Pédrot
2017-04-25Fix an optimization failure in tclPROGRESS.Pierre-Marie Pédrot
2017-04-25Merge PR#567: Fix bug #5377: @? patterns broken.Maxime Dénès
2017-04-25Merge PR#578: Fix nsatz not recognizing real literals.Maxime Dénès
2017-04-25[travis] mathcomp and fiat overlay for #402Emilio Jesus Gallego Arias
2017-04-25[location] Cleanup.Emilio Jesus Gallego Arias
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] [ast] Switch Constrexpr AST to an extensible node type.Emilio Jesus Gallego Arias
2017-04-25[location] Be consistent with type module qualificationEmilio Jesus Gallego Arias
2017-04-25[location] Document changes.Emilio Jesus Gallego Arias
2017-04-25[location] Remove `Loc.internal_ghost`Emilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Use located in tactics.Emilio Jesus Gallego Arias
2017-04-24[location] Use located in misctypes.Emilio Jesus Gallego Arias
2017-04-24[location] More located use.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 23:38:49 +0000