aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.predicate_pattern to located.Emilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.cases_pattern to located.Emilio Jesus Gallego Arias
2017-04-24[location] Use Loc.located for constr_expr.Emilio Jesus Gallego Arias
2017-04-24[constrexpr] Make patterns use Loc.located for location informationEmilio Jesus Gallego Arias
2017-04-24[toplevel] Don't check proofs in -quick mode.Emilio Jesus Gallego Arias
2017-04-24[toplevel] Don't mask critical exceptions in vernac interpretation.Emilio Jesus Gallego Arias
2017-04-24Adding a dedicated travis overlay for fiat-parsers.Pierre-Marie Pédrot
2017-04-24Removing various tactic compatibility layers in core tactics.Pierre-Marie Pédrot
2017-04-24Porting the firstorder plugin to the new tactic API.Pierre-Marie Pédrot
2017-04-24Removing compatibility layer in Leminv.Pierre-Marie Pédrot
2017-04-24Removing tactic compatibility layer in Command.Pierre-Marie Pédrot
2017-04-24Removing tactic compatibility layer in congruence.Pierre-Marie Pédrot
2017-04-24Removing tactic compatibility layer in Micromega.Pierre-Marie Pédrot
2017-04-24Fix the API of the new pf_constr_of_global.Pierre-Marie Pédrot
2017-04-24Removing trivial compatibility layer in refl_omega.Pierre-Marie Pédrot
2017-04-24Porting omega to the new tactic API.Pierre-Marie Pédrot
2017-04-24Removing trivial compatibility layer in omega.Pierre-Marie Pédrot
2017-04-24Porting generalize_dep to the new tactic engine.Pierre-Marie Pédrot
2017-04-24Removing the tclWEAK_PROGRESS tactical.Pierre-Marie Pédrot
2017-04-24Removing the tclNOTSAMEGOAL primitive from the API.Pierre-Marie Pédrot
2017-04-24Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Maxime Dénès
2017-04-24refman: remember the old name of template polymorphism.Gaetan Gilbert
2017-04-24Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.Maxime Dénès
2017-04-24Merge PR#552: Miscelaneous commitsMaxime Dénès
2017-04-24Merge PR#577: Add bedrock targets src and facade to Travis CIMaxime Dénès
2017-04-24Merge PR#569: Documenting EConstr for developpers.Maxime Dénès
2017-04-24Merge PR#565: Remove VernacErrorMaxime Dénès
2017-04-24Merge PR#580: [ide] Fix #5482 "location for query commands" in IDE.Maxime Dénès
2017-04-24Merge PR#581: [toplevel] [emacs] Don't quote errors in emacs mode.Maxime Dénès
2017-04-24Merge PR#492: [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3Maxime Dénès
2017-04-24Merge PR#576: [ide] Rely less on `Stateid.dummy`Maxime Dénès
2017-04-24[travis] Pin camlp5 to the minimal version 6.14 for 4.02.3Emilio Jesus Gallego Arias
2017-04-23[toplevel] [emacs] Don't quote errors in emacs mode.Emilio Jesus Gallego Arias
2017-04-22Merge branch v8.6 into trunkHugo Herbelin
2017-04-22Removing TODO file which is unused for more than 10 years.Hugo Herbelin
2017-04-21[ide] Fix #5482 "location for query commands" in IDE.Emilio Jesus Gallego Arias
2017-04-21Remove VernacErrorGaetan Gilbert
2017-04-21[flags] Deprecate is_silent/is_verbose in favor of single flag.Emilio Jesus Gallego Arias
2017-04-20Add bedrock targets src and facadeJason Gross
2017-04-20Fix nsatz not recognizing real literals.Guillaume Melquiond
2017-04-20Fix bug #5377: @? patterns broken.Pierre-Marie Pédrot
2017-04-20COMMENT: Pre_env.envMatej Kosik
2017-04-20COMMENT: Proof_global.pstate.pidMatej Kosik
2017-04-20refactoring "Ppvernac.pr_extend"Matej Kosik
2017-04-20correcting a typo in a commentMatej Kosik
2017-04-20correcting comments in the "Context" moduleMatej Kosik
2017-04-20"tclENV" is sexier, use it instead of "Env.get"Matej Kosik
2017-04-20reduce syntactic noiseMatej Kosik
2017-04-20simplifying "Environ.push_named" functionMatej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-11 12:09:15 +0000